# RZ: a tool for bringing constructive and computable mathematics closer to programming practice

- 21 January 2007
- Publications, RZ, Talks

With Chris Stone.

**Abstract:**

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.

Presented at Computablity in Europe 2007.

**Download paper:**

- Long version: cie-long.pdf (January 29, 2007)
- Short version: cie-short.pdf (January 29, 2007)

**Download slides:** cie2007-slides.pdf

**Download source code** from RZ web page.

**How to comment on this blog:**At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention

`andrejbauer@mathstodon.xyz`

, I will
gladly respond.
You are also welcome to contact me directly.
## Comments

The slides appear to have been corrupted, or so says my Acrobat Reader (Version 8).

Thank you for spotting this. I fixed it. If you are still getting a corrupted file, it is because your browser is holding te old version in cache.

Got the fixed version now. Thanks for being so efficient.