Swift has a rather advanced type system and offers a great set of features. I believe this makes the language suitable to explore many ideas related to static verification (e.g. capability-based systems, behavioral types, gradual typing, etc.).
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.
For example, is there a reason why Swift is significantly different than Scala from a formalization POV? Off the top of my head, many of the key type system features (broadly speaking) are similar -- classes with inheritance and subtyping, method overloading, traits+implicits vs protocols.
Say for instance one was planning on exploring the addition of uniqueness and borrowing a la Rust in Swift. Determining whether or not this would result in a sound type system can't be formally evaluated.
I think that having an operational semantics for SIL (Swift Intermediate Language) would be a great addition here.
- It would help people writing optimization passes.
- SIL doesn't change that much compared to Swift, which means there is a better chance that the operational semantics is useful for a longer time without further changes.
- Since SIL is smaller than Swift, it already has better coverage of language features in its documentation. So it might be possible to have an operational semantics for a large chunk of SIL, compared to spending the same time to design an operational semantics for a small idealized subset of Swift.
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.
From a user's point of view, I believe that a formal semantics could also ease the understanding of some of Swift's most advanced features. For instance, teaching the use of protocols and conditional conformance can prove challenging, as the rules under which Swift's type solver operates often have to be "discovered" in a kind of trial-and-error loop.
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.
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.