Formal specifications of programming languages

[Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>]

I see people have opinions about formal semantics.

Having formal semantics for a programming language is a valuable thing,
even if most people do not understand it. Such semantics is a piece of
mathematics that removes (hopefully) every doubt as to what we are
talking about, and has other benefits as well. High priests can then
write sermons in common language and explain the meaning of the Holy Word.

It would probably be quite hard to provide formal semantics for complete
ocaml, for several reasons, such as sheer size, C interface, and the
fact that it is a moving target.

But what is formal semantics good for?

Complete formal semantics written with a tool such as Coq, together with
formal proofs of its properties (existence of principal types,
uniqueness of typing, type preservation, progress lemma) is good for
automatic extraction of a prototype type-checker and/or interpreter.
This can be extremely valuable for PL researchers who want to experiment
with new features.

Incomplete formal semantics written in a series of papers and
dissertations is still quite useful. It allows researchers to clearly
express and communicate ideas. Once a person learns how to read the
mathematics that may greatly help his or her understanding of corner
cases and peculiar examples.

We (researchers) should encourage "ordinary programmers" to read formal
semantics by writing manuals and textbooks that incorporate the
formalism and decorate it with sufficient explanation.

Think about the fact that specifying concrete syntax in BNF-like
formalism has become the norm. Programmers happily read it and the
benefits are obvious. Nobody suggests that syntax should be explained in
English prose because BNF is too hard to understand. So why are you
suggesting that the norm for describing other pieces of a programming
language, such as typing rules and operational semantics, should be
primarily (or only) English prose?

Andrej