RZ
RZ is a tool for automatic generation of program specifications from definitions of mathematical theories. It was written by Chris Stone and Andrej Bauer. The purpose of RZ is to help programmers and mathematicians design data structures which properly implement mathematical structures (algebras, real numbers, Hilbert spaces, etc.)
Download
- Source code and examples: rz.tar.gz
- Binary executables:
- Browse the download directory.
Documentation
- A good starting point to learn about RZ is the paper "RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice".
- You may also browse RZ related blog posts.