Programmers are well familiar with BNF as a concise and precise formal notation for defining programming language syntax. Nobody would consider describing a grammar in prose. But more than 60 years since the invention of syntax formalisms, it’s still accepted mainstream practice that programming language semantics, which is the far more delicate part of a language definition, is routinely described by a combination of cumbersome sentences, hidden assumptions, and wishful thinking.

In this lecture, I show how the specification for WebAssembly closes this gap, hopefully demonstrating that there should be little reason to be afraid of formal semantics. It’s merely more syntax! The techniques that the academic community has developed over the past 4 decades work well, and under suitable conditions they scale to a full-blown industrial language. The primary prerequisite is that language designers embrace them from the beginning and exploit the feedback loop between design and formalisation to inform a clean semantics.