Mathematics and Computation

A blog about mathematics for computers

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

Documentation