Hello everyone! My name is George, and I'm an undergraduate computer science student at the University of California, Davis. I've been using Swift for about eight years and would love to contribute to the language that has enabled me (and many others) to build great mobile applications, HTTP servers, and more.
I'm very interested in compilers and programming languages, which is why I've been working on an exciting research project in those areas with a professor at UC Davis since June. Some of this work has involved the design of a type system enforcing certain security properties, which we will eventually implement in Rust.
As a result, I've read many papers (and one book) on type theory over the last few months, and I was curious if any mentors would be interested in the idea formalizing one of the proposed projects in addition to implementing and testing it.
Don't get me wrong - I fully understand that these projects are intended to have primarily practical value! However, there could be some benefits to formalizing and verifying them too. For example...
- Verifying the soundness of new features could convince software engineers and companies that Swift is the best choice for them compared to languages that may not be sound.
- Formalizing new features could encourage researchers to explore Swift in their own work, opening the Swift community to a larger pool of talented and knowledgeable contributors.
For some languages, this is very common! There is extensive literature on Haskell, Scheme, Standard ML, OCaml, and other functional languages (because they are the easiest to reason about). However, some more "practical" languages have also made efforts to formalize the theory underlying their compilers.
An excellent example is Kotlin, which has a spec describing its syntax and type system. Perhaps an even better example is Scala. Its creator, Martin Odersky, has published a number of papers on experimental Scala features (he may have also written about official Scala features, but I'm not sure).
The lexical scoping and macro GSoC projects seem like great candidates for this kind of exploration - do any mentors (or general community members) think this would be an interesting idea?
I understand if the consensus is no - just wanted to float the thought. Thank you for your input!
EDIT - I found this thread from a few years ago that also touches on the topic of formal semantics.