Explore a groundbreaking solution to streamline the WebAssembly (Wasm) specification process in this 16-minute conference talk from PLDI 2024. Discover SpecTec, a domain-specific language and toolchain designed to address the challenges of Wasm's growing complexity. Learn how SpecTec serves as a single source of truth, generating typeset specifications, formal definitions, prose pseudocode descriptions, and a meta-level interpreter from a unified Wasm semantics definition. Examine the tool's effectiveness in representing Wasm 2.0 and its ability to detect historical and current errors in the specification. Gain insights into the potential adoption of SpecTec by the Wasm standards community for future versions of the language.
Overview
Syllabus
[PLDI24] Bringing the WebAssembly Standard up to Speed with SpecTec
Taught by
ACM SIGPLAN