[Keynote] Keynote and SpecTec demo
summary
Wasm 3 is live with garbage collection, exception handling, tail calls, 64-bit addresses and multiple memories, and the spec is a fully end‑to‑end formalization: small‑step semantics plus a prose equivalent and zero undefined behavior. The spec is mechanized in Coq and Isabelle mechanizations (Wasm2 now, work underway for Wasm3), includes machine‑checked progress/preservation proofs, and a toolchain generates RST/PDF and prose from the formal rules; a separate test generator and smarter fuzzers are already emerging.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:47WebAssembly formal spec
- 9:14Scaling WebAssembly spec
- 20:40SpecTec for semantics
- 43:06Benefits of machine-readable specs
- 44:10Q&A on interpreter and funding
related talks
16mBringing the WebAssembly Standard up to Speed with SpecTec
01h 06mKeynote: Memory of Past and Future – Wasm’s Evolving Model of Store
29mVerification of WebAssembly Features
51mLightning Talks
57mIs Wasm Becoming Garbage? (Keynote)
01h 06mAs low-level as possible, but no lower
05mLighting talks and closing discussion
59mKeynote