From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id A8614BC0B for ; Thu, 1 Feb 2007 21:39:44 +0100 (CET) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l11Kdiiu028314 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Thu, 1 Feb 2007 21:39:44 +0100 Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id 07AC6202165; Thu, 1 Feb 2007 21:39:44 +0100 (CET) Received: from serveur9-10.lri.fr (serveur9-10 [129.175.9.10]) by smtp.lri.fr (Postfix) with ESMTP id 30348CED98; Thu, 1 Feb 2007 21:39:41 +0100 (CET) Received: from filliatr by serveur9-10.lri.fr with local (Exim 3.36 #1 (Debian)) id 1HCiib-0004yG-00; Thu, 01 Feb 2007 21:39:41 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <17858.20493.719512.768499@serveur9-10.lri.fr> Date: Thu, 1 Feb 2007 21:39:41 +0100 From: Jean-Christophe Filliatre To: "Chris King" Cc: Andrej.Bauer@andrej.com, oleg@pobox.com, caml-list@inria.fr Subject: Re: [Caml-list] Re: Programming with correctness guarantees In-Reply-To: <875c7e070702010500p5f08cf4bh1349234de1caef83@mail.gmail.com> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <45C1A8B5.3090002@fmf.uni-lj.si> <875c7e070702010500p5f08cf4bh1349234de1caef83@mail.gmail.com> X-Mailer: VM 7.19 under Emacs 21.4.1 X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at discorde with ID 45C25010.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 filliatr:01 lri:01 lri:01 coq:01 o'caml:01 pointers:01 ocaml:01 assertions:01 syntactic:01 writes:01 caml-list:01 simplify:01 constructs:02 programming:03 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