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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 25A1FBC0B for ; Thu, 1 Feb 2007 21:12:04 +0100 (CET) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l11KC3Nx019262 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Thu, 1 Feb 2007 21:12:03 +0100 Received: from smtp.lri.fr (serveur3-5 [129.175.3.5]) by ext.lri.fr (Postfix) with ESMTP id 85D32202164; Thu, 1 Feb 2007 21:12:03 +0100 (CET) Received: from serveur9-10.lri.fr (serveur9-10 [129.175.9.10]) by smtp.lri.fr (Postfix) with ESMTP id 2EE3CCED98; Thu, 1 Feb 2007 21:12:01 +0100 (CET) Received: from filliatr by serveur9-10.lri.fr with local (Exim 3.36 #1 (Debian)) id 1HCiHp-0004Ps-00; Thu, 01 Feb 2007 21:12:01 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <17858.18833.95585.840472@serveur9-10.lri.fr> Date: Thu, 1 Feb 2007 21:12:01 +0100 From: Jean-Christophe Filliatre To: "Joshua D. Guttman" Cc: oleg@pobox.com, caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si Subject: Re: [Caml-list] Programming with correctness guarantees In-Reply-To: References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> X-Mailer: VM 7.19 under Emacs 21.4.1 X-Virus-Scanned: by amavisd-new at lri.fr X-Miltered: at concorde with ID 45C24993.003 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; filliatre:01 filliatr:01 lri:01 oleg:01 frightening:98 writes:01 writes:01 caml-list:01 programming:03 seems:03 unit:03 unit:03 guttman:04 applied:04 somewhere:05 Joshua D. Guttman writes: > oleg@pobox.com writes: > > > I remember reading somewhere that after a division of > > Siemens applied this technique to a high assurance > > project, they noted an exhilarating feeling of being > > able to program without unit tests. The code was correct > > by construction. > > This seems really frightening. 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?'' More seriously, I heard a similar remark from a French company which formally verified the embedded code of an automatic subway line (using the B method). They explained that, after the verification had been completed, the unit phase was not suppressed, but greatly reduced. -- Jean-Christophe