Generating Executable Specification from Formal Semantics of WebAssembly
summary
Generates an executable specification pipeline from the Wasm DSL into an algorithmic representation and a meta-level interpreter, producing the prose spec and back ends automatically. The generated interpreter passes the official Wasm unit tests (excluding SIMD) in 21 seconds; SIMD support later reaches 86% pass with 14% remaining. The tool also fuzzes by generating 10,000 tests in minutes, finds real bugs in implementations, and reports coverage gaps (memory/table copy).
AI-written summary · about
chapters (17)
- 0:00Executable WebAssembly semantics
- 3:56Formal semantics importance
- 9:14JavaScript to WebAssembly semantics
- 12:50WebAssembly semantics differences
- 15:59Single-source-of-truth vision
- 23:40Interpreter validation with tests
- 27:11Current spec status and errors
- 30:23Test suites for WebAssembly
- 33:44Coverage limits and improvements
- 36:39Beyond WebAssembly to other languages
- 39:29Community impact and future
- 40:12Q&A: Compilers and type checkers
- 42:40Q&A: Other spec frameworks
- 46:55Q&A: Evaluation contexts in DSL
- 48:03Q&A: Generated prose in specs
- 51:12Q&A: DSL specialization vs generalization
- 53:02Q&A: Prose versus standards
related talks
16mBringing the WebAssembly Standard up to Speed with SpecTec
01h 06mAs low-level as possible, but no lower
01h 08mOn WebAssembly
32mWebAssembly: birth of a virtual ISA
57mBusy Developer’s Guide to WebAssembly
35mWebAssembly: now web is a new compiler target architecture
42mWebAssembly: A New Compilation Target for the Web
37mDecoding the hype behind WebAssembly: Looking under the hood