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=AWL 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 AD3CEBC0B for ; Fri, 2 Feb 2007 06:47:33 +0100 (CET) Received: from ipmail01.adl2.internode.on.net (ipmail01.adl2.internode.on.net [203.16.214.140]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l125lUur024578 for ; Fri, 2 Feb 2007 06:47:32 +0100 Received: from ppp27-234.lns1.syd6.internode.on.net (HELO rosella) ([59.167.27.234]) by ipmail01.adl2.internode.on.net with ESMTP; 02 Feb 2007 16:17:08 +1030 X-IronPort-AV: i="4.13,272,1167571800"; d="scan'208"; a="82700191:sNHT13438378646" Subject: Re: [Caml-list] Programming with correctness guarantees From: skaller To: Jean-Christophe Filliatre Cc: Robert Fischer , caml-list@inria.fr In-Reply-To: <17858.21560.812318.17915@serveur9-10.lri.fr> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <17858.18833.95585.840472@serveur9-10.lri.fr> <54337.151.151.73.165.1170362159.squirrel@webmail.fischerventure.com> <17858.21560.812318.17915@serveur9-10.lri.fr> Content-Type: text/plain Date: Fri, 02 Feb 2007 16:47:05 +1100 Message-Id: <1170395225.19859.85.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.6.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 45C2D072.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; 0100,:01 filliatre:01 model:01 sourceforge:01 wrote:01 imho:01 caml-list:01 theorem:02 prover:02 programming:03 thu:05 provers:05 programmer:06 correctness:08 correctness:08 On Thu, 2007-02-01 at 21:57 +0100, Jean-Christophe Filliatre wrote: > This is a statement easily established by most automatic provers. Then > there is no need testing function min anymore, since it has been > proved correct for _any_ input values. This isn't right, IMHO: there is still need to test: after all the proof itself, and the theorem prover, the operating system, etc, all introduce additional risks. The point is that you no longer rely solely on the WORST possible way of guessing if a program is going to work: testing. Instead you rely on BOTH proof and testing, and you can put a lot more effort (money) into the proof than the testing to get the best results. But you never forget to actually test the code too! Don't forget that even with perfect machine model .. the actual specification may be wrong! Correctness isn't enough! The program has to actually work! But now, you can more easily blame the spec writer than the programmer if it doesn't ... :) -- John Skaller Felix, successor to C++: http://felix.sf.net