Sometimes building a language is the best solution to a problem. This takes on many forms, from designing DSLs to implement an OS shell to more ambitious languages for verifying filesystems. Since we’re in the Golden Age of PL Research, there are plenty of reasons to give language design a try!
Languages are foundational, though, and soundness issues in them affect all of their programs. This makes them a great candididate for formalization and verification, since the cost of errors is very high, but as usual that means we have to address the verification gap. In this post we’ll cross the gap by building and (partially) verifying an operational semantics of a small language in Isabelle/HOL, and we’ll extract this semantics into an executable interpreter in OCaml.
The Language: Boolean Expressions
Let’s keep the language simple to focus on the end-to-end process of extraction. Our language will allow expressing and evaluating boolean expressions and conditionals, like “if true then true else false” (this is just the untyped boolean expression language from Chapter 3 of Types and Programming Languages).
First, we define the (abstract) syntax, in Isabelle: