Version française
Home     About     Download     Resources     Contact us    
Browse thread
Programming with correctness guarantees
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jean-Christophe Filliatre <filliatr@l...>
Subject: Re: [Caml-list] Re: Programming with correctness guarantees

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