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 1D990BC0B for ; Thu, 1 Feb 2007 14:07:42 +0100 (CET) Received: from smtp-bedford.mitre.org (smtpproxy1.mitre.org [192.160.51.76]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l11D7fXq012701 for ; Thu, 1 Feb 2007 14:07:41 +0100 Received: from smtp-bedford.mitre.org (localhost.localdomain [127.0.0.1]) by smtp-bedford.mitre.org (8.12.11.20060308/8.12.11) with SMTP id l11D7dO8018932 for ; Thu, 1 Feb 2007 08:07:39 -0500 Received: from smtp-bedford.mitre.org (localhost.localdomain [127.0.0.1]) by smtp-bedford.mitre.org (Postfix) with ESMTP id DD139BF00 for ; Thu, 1 Feb 2007 08:07:38 -0500 (EST) Received: from linus.mitre.org (linus.mitre.org [129.83.10.1]) by smtp-bedford.mitre.org (8.12.11.20060308/8.12.11) with ESMTP id l11D7cfS018923; Thu, 1 Feb 2007 08:07:38 -0500 Received: from oolong.mitre.org (oolong.mitre.org [129.83.162.16]) by linus.mitre.org (8.12.11/8.12.10) with ESMTP id l11D7bgK023882; Thu, 1 Feb 2007 08:07:37 -0500 (EST) To: oleg@pobox.com Cc: caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si, guttman@mitre.org (Joshua D. Guttman) Subject: Re: [Caml-list] Programming with correctness guarantees Reply-To: guttman@mitre.org (Joshua D. Guttman) References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> From: "Joshua D. Guttman" Date: Thu, 01 Feb 2007 08:07:37 -0500 In-Reply-To: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> (oleg@pobox.com's message of "Wed, 31 Jan 2007 21:04:31 -0800 (PST)") Message-ID: User-Agent: Gnus/5.11 (Gnus v5.11) Emacs/22.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Miltered: at discorde with ID 45C1E61D.004 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; oleg:01 model:01 compiler:01 formalized:01 formalized:01 ocaml:01 frightening:98 writes:01 caml-list:01 supported:01 instances:02 match:02 namely:02 linking:02 constraints:03 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. Don't the unit tests also serve another purpose, namely to confirm that the formal model of the software environment is correct? That is, that all of the libraries you're linking against (and the compiler itself) are behaving in a way that matches the expectations you formalized? As well as a concrete confirmation that the formalized ideas match correctly against what you really wanted in specific instances: the formal insight of human beings is imperfect. (:-) I hope that the words "exhilarating feeling" were meant to indicate that they didn't really do this, but had the impression that they could *almost* do so. You don't want to lose contact with the real world constraints when programming in a formally supported way. I suppose that this doesn't really have much to do with OCaml; apologies. Joshua -- Joshua D. Guttman The MITRE Corporation