Lambda the Ultimate

RZ for Constructive Mathematics in Programming by Chris Stone and Andrej Bauer.

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.

I haven't read the paper yet, but the abstract reminded me of PADS.

I have begun a new weblog on which I will gradually disgorge all of the inner knowledge of the design and use of my NML language. NML was first developed back in 1999 while at Raytheon, and then grown organically over these past 7 years of constant use.

NML is a vectorized math language akin to MatLab, but overtly functional, with a very strong similarity to OCaml syntax. However, like Lisp, it is dynamically typed and inherently "unsafe".

Our uses are primarily aimed at signal and image processing, but NML has been used for all kinds of numerical modeling efforts, and it continues to be used for predictive analysis of natural systems.

All interested parties are welcome.