Lambda the Ultimate

RZ: a tool for bringing constructive and computable mathematics closer to programming practice, Chris Stone and Andrej Bauer.

Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

Realizability is a way of formalizing the constructive interpretation of logical formulas (eg, the BHK interpretation). Constructively, a proof of an implication A implies B means that if you are given evidence for A, you must be able to compute evidence for B. Since this constructive interpretation does not specify any particular programming language (theorists often use the lambda calculus, Turing machines, and the like) so Andrej Bauer and Chris Stone observed that they could take the realizers of mathematical proofs to be Objective Caml programs! This meant that they could take mathematical theories and generate ML module signatures describing the interface to the implementation of a mathematical theory, plus comments about what invariants must hold.