RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice

Realizability theory is not just a fundamental tool in logic and computability. It also has direct application to the design and implementation of programs, since it can produce code 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.