Programmers are well familiar with BNF as a concise and precise formal
notation for defining programming language syntax. Nobody would
consider describing syntax in prose. But more than 60 years after the
introduction of syntax formalisms, it’s still accepted practice that
programming language semantics, which is the far more delicate part
of a language definition, is specified by a combination of cumbersome
prose, hidden assumptions, and wishful thinking.
In this talk, I show how we closed this gap in the specification of
WebAssembly, hopefully demonstrating that there is little reason to be
afraid of formal semantics. In the end, it’s merely syntax! The
techniques that the academic community has developed over the past 4
decades work well and scale to a full-blown industrial language. I
also give a peek at a novel tool chain this approach enables us to
build, which can generate much of the written WebAssembly
specification and corresponding proofs and tests, achieving new levels
of trust in the correctness of the specification.