SODA: A Language for Executable Semantics

SODA is a domain-specific language for writing, running and comparing operational, denotational and axiomatic semantics. Language designers define syntax once and use it for execution rules, semantic functions and proofs. SODA evaluates these definitions, displays derivations and checks proof certificates. We demonstrate their agreement for a language with assignments, conditionals and local variables. Lean proofs establish operational–denotational correspondence, soundness and relative completeness of its Hoare rules, and exact symbolic weakest preconditions. A checker validates results exported by SODA against this model. An account-transfer program applies the theorems to prove conservation of balances across arbitrary finite batches. Repository: https://github.com/soda-lang-project/SODA