WebAssembly Unleashed WebAssembly SpecTec | WebAssembly Unleashed
6 snips
May 12, 2025 
Andreas Rossberg, a programming languages researcher and co-designer of the WebAssembly specification, joins the conversation to share his journey from V8 to WebAssembly. He introduces SpecTec, a unique language designed to unify and streamline the WebAssembly specification. The discussion reveals how SpecTec addresses duplication issues and enhances compiler construction. Andreas also touches on the unexpected adoption of WebAssembly in embedded systems and emphasizes the need for improved tooling and runtimes in the community.
AI Snips
Chapters
Transcript
Episode notes
Early SML Sparked Formalization Interest
- Andreas fell into functional programming during university after seeing Standard ML and its formalized semantics.
- The formal specification approach in SML inspired his interest in precise language definitions.
SpecTec As Single Source Of Truth
- SpecTec is a domain-specific language that serves as a single source of truth for WebAssembly's syntax, semantics, prose, and proofs.
- It generates LaTeX, Coq, prose, and a meta-interpreter to reduce duplicate manual work and increase specification assurance.
Centralize Specs To Cut Manual Work
- Focus specification work on a single authoritative source to avoid duplicated prose, LaTeX, and Coq translations.
- Use automated backends to reduce manual review overhead and increase confidence in proofs.