Formal Semantics for Top 5 Programming Languages

A recent blog post on undefined behavior in C got me thinking. Being from the ML community, I have a certain appreciation for rigorous formal semantics that can be machine checked. Though practical machine checking is largely a new development, rigorous formal semantics has been with us for decades. Standard ML is the epitome of this approach to language design. The 48-page (128-pp total when including appendices and TOC/index) The Definition of Standard ML - Revised formally specifies the entirety of the language¹. Don't get me wrong. The Standard isn't perfect. Indeed, it has some bugs of its own [PDF]. Nevertheless, for the most part, the Standard has raised the level of discourse and enabled succinct yet precise descriptions of a powerful higher-order typed language possible. This approach to modeling, defining, and evolving programming languages has in recent years taken a life of its own having been applied to both new experimental languages as well as time-tested existing languages.

Data-Driven Language Design

One recurring issue with the evolution of programming languages is the tension between feature creep and stagnation. Some programming languages manage to evolve very rapidly, incorporating all kinds of features in response to developer requests or the language architect's leading. Brian Goetz has an interesting article on DeveloperWorks which argues for using "corpus analysis", studying the actual frequency of use of language constructs in the corpus of source code, to guide the evolution of a language. In his article, he describes two examples, precise exceptions rethrow semantics and type inference, where corpus analysis played a role in determine how Java evolved. When I was working on SML/NJ, we informally used this technique to determine the best design in terms of certain type checking/inference and module system elements.