Production Language Specification - Requirements for Multiple Usages
summary
Argues that one meta-language cannot serve all needs and surveys concrete tooling: LATeX/OCaml/Isabelle/HOL backends from LEM, a domain‑specific Sale front end that generates Rust and verifier backends, and lightweight translators that work for executable specs and test oracles. Reports success: LEM works well for execution and ISA models but produces non‑idiomatic prover code; Sale generates useful production code for instruction semantics. Identifies recurring failures: variable binding, robust production parser generation, module systems, partiality and lightweight dependent types.
AI-written summary · about
chapters (10)
- 0:00Language spec challenges
- 3:56Problems of success
- 8:31User-definable syntax tooling
- 13:27Variable binding and scoping
- 14:54Parsing context-free grammars
- 16:26Inductive relations and meta-language
- 19:59Sail instruction set semantics
- 21:04Undergraduate semantics tooling
- 22:52Future directions
- 23:13Closing remarks
related talks
32mA Survey of Weak Reasoning Assistants
29mLegalese: Software Eats Contract Drafting
24mSpeculative Development
51mHow to Cultivate a Language
29mA New Standard ML Prettyprinter Library, An Experience Report
20mA Core Calculus for Documents: Or, Lambda: The Ultimate Document
05m“Validating Lemmas with Rustdoc [...]”
45mAdding Testable Code Specifications in the Linux Ke...