Programming Languages Must Have Formal Semantics. Period.

on YouTube ↗31m

" summary

Argues that every language gets a machine-checkable formal semantics first and that all tools—interpreter, compiler, verifier, model checker—are automatically derived from it using the K framework. Shows an executable semantics for kernel C with about 120 cells and >5,000 semantic rules, and a K implementation of many real languages; K itself is ~500k LOC. Demonstrates modular rewrite rules (contextual cells), tool regeneration by re-running the semantics, translation‑validation proofs and a tiny proof checker to make K trustless, noting runtimes ~one order of magnitude slower.

AI-written summary · about

" chapters (9)

1. 0:00Introduction
2. 1:04Modern software complexity
3. 3:56Language tool challenges
4. 8:51Semantics-first design
5. 14:31K framework cells
6. 19:54Executable formal semantics
7. 21:20Trustless K with translation
8. 24:07Deriving tools from semantics
9. 30:05Q&A

" related talks

• 01h 03mMatching Logic: Foundation of the K FrameworkGrigore Rosu · CPP 2020
• 40mFormal semantics for multi-language programsAmal Ahmed · PWLConf 2023
• 40mFormal semantics for multi-language programsAmal Ahmed · Strange Loop 2023
• 16mExtrinsically Typed Operational Semantics for Functional LanguagesJeremy G. Siek, Dale Miller, Matteo Cimini · SLE 2020
• 18mThe Essence of Verilog: A Tractable and Tested Operational Semantics for Verilo...Yue Li, Tian Tan, Qinlin Chen, Nairen Zhang, Jinpeng Wang, Chang Xu, Xiaoxing Ma · OOPSLA 2023
• 31mFormal SpecificationThomas Bourgeat · 8th RISC-V Workshop Barcelona 2018
• 21mSynthesizing Formal Semantics from Executable InterpretersLoris D'Antoni, Thomas Reps, Jiangyi Liu, Charlie Murphy, Anvay Grover, Keith J.C. Johnson · OOPSLA 2024
• 20mCertified Abstract Machines for Skeletal SemanticsGuillaume Ambal, Serguei Lenglet, Alan Schmitt · CPP 2022