This paper explores why Abstract Machine Semantics is easier to use in formal development than traditional Small-step Semantics (also called SOS for Structural Operational Semantics) when mechanizing programming languages. This choice of semantics has been used in multiple large-scale mechanizations, like CompCert, or CakeML, but without comparison of the two approaches.
We show that once spurious or trivial cases (that would not appear in a pen-and-paper proof) are proven automatically, Abstract Machine Semantics leads to a smaller number of cases to do by hand in comparison with Small-Step Semantics. This advantage is very important when considering an evolving development, where proofs need to be re-written multiple times.
The reduced burden of proofs by hand in Abstract Machine Semantics can be explained by two factors
- a simple induction principle
- a syntactic-deterministic semantic, that permits to use built-in automation tools like
constructororinversionefficiently without spurious cases generation.
In addition to the explanations, we provide a Rocq artifact on a mid-size programming language mechanization for the Catala programming language.
For more information, you can read the paper and send me a question.
This work was done while working in the Prosecco and Epicure teams together with Sandrine Blazy and Denis Merigoux.
I will present this work at PPDP2025.