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=1.0 required=5.0 tests=AWL,SPF_NEUTRAL 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 76FE9BC69 for ; Thu, 1 Feb 2007 14:08:14 +0100 (CET) Received: from wx-out-0506.google.com (wx-out-0506.google.com [66.249.82.237]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l11D1pJS011394 for ; Thu, 1 Feb 2007 14:02:13 +0100 Received: by wx-out-0506.google.com with SMTP id i31so493510wxd for ; Thu, 01 Feb 2007 05:00:54 -0800 (PST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=CSbvLB5p2FyZ8QySRvAI0RnB1GUp1uwOM7zn1B2UiZ7c/trbdPJDTo6AJeQhc5Ejc1dNtzoPq8tZiTS6zvOVKJG2nH8ymgImwuCXJPSY97SartBDRoCRLHm07z5eKmUnHB8cawJkDZHDvj8uNlZWX95ZntyEIaJUrwpx3PSJMmA= Received: by 10.90.68.15 with SMTP id q15mr3122000aga.1170334852032; Thu, 01 Feb 2007 05:00:52 -0800 (PST) Received: by 10.90.55.5 with HTTP; Thu, 1 Feb 2007 05:00:51 -0800 (PST) Message-ID: <875c7e070702010500p5f08cf4bh1349234de1caef83@mail.gmail.com> Date: Thu, 1 Feb 2007 08:00:51 -0500 From: "Chris King" To: Andrej.Bauer@andrej.com Subject: Re: [Caml-list] Re: Programming with correctness guarantees Cc: oleg@pobox.com, caml-list@inria.fr In-Reply-To: <45C1A8B5.3090002@fmf.uni-lj.si> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <45C1A8B5.3090002@fmf.uni-lj.si> X-j-chkmail-Score: MSGID : 45C1E4BF.000 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 45C1E4BF.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lri:01 coq:01 o'caml:01 assertions:01 caml-list:01 simplify:01 programming:03 chris:06 chris:06 engines:93 correctness:08 translates:10 procedure:11 such:14 language:15 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