Whoa, very cool post! It's interesting that "small but novel" languages can be formally proved. Do any mainstream languages have a sound foundation like that? If someone is interested in creating a new programming language, is it worth getting up to speed on proof writing and using that to build the language? It's not really a topic that comes up in the Dragon Book or mainstream general compiler study, AFAIK.
> Do any mainstream languages have a sound foundation like that?
I can think of a few languages that started from a formal theory (e.g., Eff [1]), but none of them are "mainstream". There was a mostly successful attempt [2] at formally specifying C and implementing a verified compiler for it. Standard ML has a very comprehensive spec [3], perhaps the best of any "mainstream" language. It's not quite at the level of a Coq formalization, but also not too removed from it. Haskell is based on a lot of peer-reviewed papers, but there isn't one comprehensive spec for it at this level of formalism. Also, the RustBelt project [4] is worth mentioning. It's an initiative to develop a formal theory of Rust.
> If someone is interested in creating a new programming language, is it worth getting up to speed on proof writing and using that to build the language?
If your new programming language contains a novel idea that you want to have published in a peer-reviewed journal/conference, then yes, I think it is absolutely worth it. It's likely your paper will be rejected without having formal proofs.
But if you don't intend to publish your ideas, it's really quite a lot of work and might not be worth it. Depends on how dedicated you are, and how much you care about things like soundness.
