Every programmer is familiar with BNF as a concise and precise formal notation for defining programming language syntax — nobody would consider describing a grammar in prose. Yet, almost 60 years since the invention of syntax formalisms, we still accept it as a given (in the “real world”) that programming language semantics, which is the far more delicate part of a language definition, is routinely described by a combination of clumsy sentences, hidden assumptions, and wishful thinking.

In this talk I will show how we successfully applied standard formal methods to WebAssembly, hopefully demonstrating that there is little reason to be afraid of it. It’s merely more syntax! The techniques that the academic PL 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 the language designers embrace them from the beginning. Then the feedback loop between design and formalisation leads to cleaner and simpler semantics. This works especially well for languages such as ILs and VMs, which are not distracted by superficial user ergonomics.