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.4 required=5.0 tests=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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 56935BC0B for ; Fri, 2 Feb 2007 01:47:47 +0100 (CET) Received: from defout.telus.net (defout.telus.net [204.209.205.55]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l120lj2R029984 for ; Fri, 2 Feb 2007 01:47:46 +0100 Received: from priv-edmwaa06.telusplanet.net ([154.20.161.125]) by priv-edmwes34.telusplanet.net (InterMail vM.7.05.01.01 201-2174-106-103-20060222) with ESMTP id <20070202004743.IETJ619.priv-edmwes34.telusplanet.net@priv-edmwaa06.telusplanet.net> for ; Thu, 1 Feb 2007 17:47:43 -0700 Received: from localhost.localdomain (d154-20-161-125.bchsia.telus.net [154.20.161.125]) by priv-edmwaa06.telusplanet.net (BorderWare MXtreme Infinity Mail Firewall) with ESMTP id EC6AJ6EKL3 for ; Thu, 1 Feb 2007 17:47:42 -0700 (MST) Received: from a6b37331 by localhost.localdomain with local (Exim 4.50) id 1HCmRm-0007B0-4f for caml-list@yquem.inria.fr; Thu, 01 Feb 2007 16:38:34 -0800 Date: Thu, 1 Feb 2007 16:38:33 -0800 From: Bob Williams To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Programming with correctness guarantees Message-ID: <20070202003833.GA27581@telus.net> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <17858.18833.95585.840472@serveur9-10.lri.fr> <45C250D8.7010700@mcmaster.ca> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <45C250D8.7010700@mcmaster.ca> User-Agent: Mutt/1.5.13 (2006-08-11) X-Miltered: at concorde with ID 45C28A31.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 telus:98 wrote:01 wrote:01 caml-list:01 programming:03 jacques:03 jacques:03 thu:05 roman:94 formal:07 correctness:08 correct:08 feb:09 methods:12 On Thu, Feb 01, 2007 at 03:43:04PM -0500, Jacques Carette wrote: > Jean-Christophe Filliatre wrote: > >There's a joke around in the formal methods community: ``would you > >prefer to get on a plane whose software has been proved correct or > >has been tested?'' > > > I heard, from someone working on an automated train system, that > everyone working on the system was required to be on the inaugural run > of said train. > > I would trust such "people methods" even more than proof and testing! > > Jacques This reminds me of the Roman Empire system: the first person to cross a new bridge was the engineer who built it!