Is there a specific reason for picking Swift in particular? For example, there has already been a bunch of formalization work related to Flow, Pony, Rust, Haskell and OCaml (all of which have advanced type systems), which might help you get off the ground quicker. With Swift, you'd have to lay the groundwork yourself.
There is indeed a great body of work in various programming languages, like those that you mentioned, and many others. My impression is that Swift's adoption outside of the academic community is slightly larger (probably with the notable exception of Haskell and Rust in your list), and addresses more industry-oriented applications. The idea of developing/adapting a verification technique to help Swift developers debug/improve their mobile apps is extremely compelling (although quite ambitious).
Swift might be an interesting subject depending on the feature being investigated. I mentioned the addition of reference uniqueness, which would be rather pointless to evaluate in languages like Rust or Pony that already have it. On the other hand, Swift is relatively permissive in its treatment of aliasing, which poses interesting challenges as to identify the minimal requirements to guarantee specific reference properties.
Swift is also one of the rare "modern" programming languages that does not primarily allocate everything onto the heap (with the notable exception of Rust). Consequently, this makes it a good candidate to evaluate features based on statically determinable lifetimes, as opposed to GCed languages based on the JVM (e.g. Scala).
And finally, though that last point is admittedly rather irrelevant, I'm quite fond of the language.
I think that having an operational semantics for SIL (Swift Intermediate Language) would be a great addition here.
It might indeed, specifically for the operational semantics. I am however not familiar enough with SIL to determine whether or not its formalization would be relevant to reason about Swift's type system. Any insights in that regards would be much appreciated.
Another avenue that might be worth exploring is designing a formal memory model. @lorentey has been working on atomics, so you might consider discussing this idea with him. He has also authored a new pitch here which is related.
Thank you for this pointer. I'll look into it.
I have a couple of hunches here:
- When teaching Swift's advanced features, the lack of formal semantics is not the core issue, or even one of the primary issues.
- Most practitioners would find learning from a formal semantics more intimidating compared to learning through examples and exercises.
I don't completely agree with that position. While seasoned practitioners with prior experience in other languages might get up to speed with examples and exercises rather quickly, my observation is that this process is much harder for students. Often, they lack the hindsight to understand the mechanisms beyond the scope of a single example/exercise, in particular when faced with advanced features, as they tend to learn new concepts syntactically only. While a formal semantics can definitely be scary at the first encounter, my experience in class have lead me to believe that it eventually helps students building a deeper understanding of the mechanisms, less tightly linked with the syntax.
Admittedly, my opinion is completely biased by my academic background and disturbing affection for inference rules.
To be clear, I'm not trying to dissuade you from writing a formal semantics for a (subset of) Swift. All I'm saying is, in my opinion, I think there might be other avenues to explore that might be more beneficial from a compiler implementation perspective.
The purpose of my post was precisely to spark similar discussions and gather this kind of comments. Yours are much appreciated.