Keynote: Who’s Afraid of the Turnstile? (bobkonf2024)

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. about this event: https://bobkonf.de/2024/rossberg.html