Hello fellow Swift enthusiasts,
TL;DR; Is there a formal definition of Swift's semantics somewhere? If not, would it be of any use to you, and in which way? If such formal semantics were to be developed, what essential aspects should it include, as opposed the features that could be abstracted away?
I am a researcher at University of Geneva, working on programming languages. In an effort to use Swift as a basis to study the practicality of new/revisited theoretical concepts, I would love to have a formal definition of Swift, or subset thereof.
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.). But a proper assessment of the soundness of a particular addition would require a formal definition of Swift's type system and operational semantics. To the best of my knowledge, such formal definitions do not exist, as Swift's semantics is expressed in prose only, in the language manual and/or in the various proposals produced by Swift Evolution.
Purely from a researcher's point of view, this hinders the use of Swift as a target to explore theoretical concepts, as correctness can only be evaluated empirically with an actual implementation. 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.
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.
Provided a formal definition of Swift's semantics hasn't indeed be formally defined yet, I plan on writing one. Consequently, I would be interested to know whether such an effort could be useful to the community. Similar projects have been carried out for other programming languages. A noteworthy example is Featherweight Java (FJ) . FJ is a minimal core calculus that aims to capture the essence of Java, precisely for the purpose of exploring the relationship between Java's semantics and other language features. For instance, FJ does not even have assignments, and focus essentially on Java's type system.
My goal is to develop a comparable minimal framework for Swift. Hence, I would be interested to know what you would consider to be the essence of Swift. My opinion is that it should also focus primarily on Swift's type system, with a strong emphasis on the difference between value and reference types.
 Igarashi, Atsushi, Benjamin C. Pierce, and Philip Wadler. "Featherweight Java: a minimal core calculus for Java and GJ." ACM Transactions on Programming Languages and Systems (TOPLAS) 23.3 (2001): 396-450.