BROADCASTS.com

Programmers are well familiar with BNF as a concise and precise formal\nnotation for defining programming language syntax. Nobody would\nconsider describing syntax in prose. But more than 60 years after the\nintroduction of syntax formalisms, it\u2019s still accepted practice that\nprogramming language semantics, which is the far more delicate part\nof a language definition, is specified by a combination of cumbersome\nprose, hidden assumptions, and wishful thinking.\n\nIn this talk, I show how we closed this gap in the specification of\nWebAssembly, hopefully demonstrating that there is little reason to be\nafraid of formal semantics. In the end, it\u2019s merely syntax! The\ntechniques that the academic community has developed over the past 4\ndecades work well and scale to a full-blown industrial language. I\nalso give a peek at a novel tool chain this approach enables us to\nbuild, which can generate much of the written WebAssembly\nspecification and corresponding proofs and tests, achieving new levels\nof trust in the correctness of the specification.\n\n\n\t\nabout this event: https://bobkonf.de/2024/rossberg.html