The Caml Hump: Focalize

FoCaLize is an integrated development environment to write high integrity programs and systems. It provides a purely functional language to formally express specifications, describe the design and code the algorithms. Within the functional language, FoCaLize provides a logical framework to express the properties of the code. A simple declarative language provides the natural expression of proofs of those properties from within the program source code.