Who’s Afraid of the Turnstile?

(And why we weren’t for WebAssembly)

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.

Andreas Rossberg

Andreas Rossberg is an independent researcher and engineer. By a few twists of fate, he became one of the designers of WebAssembly, author of its formalisation and specification, and is champion of various proposals for enhancements. In the old days he worked at Google on V8, the JavaScript/Wasm virtual machine, and spent years on TC39, the JavaScript committee. Before his time in industry he did a post-doc at the Max Planck Institute for Software Systems. His research interests mainly revolve around programming languages, ranging from foundational theory, over design, to implementation. Naturally, he also is a functional programmer.