Re: [Caml-list] Re: Programming with correctness guarantees

[Jean-Christophe Filliatre <filliatr@lri.fr>]

Chris King writes:
 > You may also be interested in Why (http://why.lri.fr/).  It is an
 > ML-ish language which allows pre- and postconditions to be specified
 > and translates those assertions into input to a variety of proof
 > engines (such as the proof assistant Coq or the decision procedure
 > Simplify).  You can then extract your code as O'Caml.

Many thanks for the advertisement :-)

But before anybody rushes to download it, I want to say that the Why
tool mostly borrows ML syntactic constructs, but is far from being a
language to specify and verify real ML programs. 

It is actually rather some kind of WHILE language, without aliasing,
that we use as an intermediate language to do verification of (real,
this time) C and Java programs, through suitable models of pointers
and memory layout.

Specifying and verifying real ML programs is currently ongoing
work in many research teams and there is no doubt we'll eventually
be able to formally verify Ocaml programs.

-- 
Jean-Christophe