Archives of the Caml mailing list > Message from Chris King

Browse thread

Programming with correctness guarantees

oleg@p...
- Andrej Bauer
  - Chris King
    - Jean-Christophe Filliatre
- Joshua D. Guttman
  - Jean-Christophe Filliatre
    - Robert Fischer
      - Jean-Christophe Filliatre
        
        skaller
    - Jacques Carette
      - Bob Williams
- Jean-Christophe Filliatre
  - Tom
- David MENTRE

Date:	-- (:)
From:	Chris King <colanderman@g...>
Subject:	Re: [Caml-list] Re: Programming with correctness guarantees

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.

- Chris King