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.)



1 thought on “RZ

  1. There is something I don’t understand here: a mathematical theory is a specification.

    So I gather this is an automated translation step from one very rich formalism (mathematical theories) to a simpler one (signatures in this case). Very useful indeed, since this is a rather boring thing to do by hand, basically because it can be automated!

    Is the back-end generator easily replaceable? It might make sense to be able to target other languages than just ocaml, in the long run.

Leave a Reply

Your email address will not be published. Required fields are marked *