Panel: Mechanized Specifications for Real-World Programming Languages
summary
Panelists contrast concrete outcomes: an K framework built for engineering-first, executable semantics; a call for a usable symbolic executor for P4 that can chain across devices; a testing tool MIRI that finds undefined behavior by running real Rust code and drives the design of mini rust; ES Meta that auto-derives mechanizations from the spec; honest limits — generated reference interpreters work but are slower than hand‑tuned production compilers and adoption is mostly a human process.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:08K framework unique aspects
- 5:46Automated reasoning for P4
- 9:38ES Meta and JavaScript spec
- 12:48Tooling for practical specs
- 19:10Why formal semantics matter
- 22:24K framework users examples
- 25:32Formal semantics for P4
- 27:42ECMAScript spec approach
- 30:09Formal vs natural language
- 34:47Generating implementations
- 38:40Standardization body methods
- 43:02Making specs accessible
- 45:54Community adoption challenges
- 47:20Shared vocabulary in specs
- 48:42First steps in writing spec
- 51:14Advice for PL researchers
- 54:09Closing remarks
related talks
29mLegalese: Software Eats Contract Drafting
32mA Survey of Weak Reasoning Assistants
45mAdding Testable Code Specifications in the Linux Ke...
38mAgile, Lean & Rugged - The Paper Edition
39mDeveloper’s Torment: The Documentation
37mDiscussion of tooling ecosystem and gaps
36mWriting Valuable Papers
08mExample-driven development: bridging tests and documentation