From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA15780; Fri, 1 Oct 2004 11:19:06 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA18154 for ; Fri, 1 Oct 2004 11:19:05 +0200 (MET DST) Received: from mail.dcs.qmul.ac.uk (vicar.dcs.qmul.ac.uk [138.37.95.146]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i919J44p008014 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 1 Oct 2004 11:19:05 +0200 Received: from xenografia.plus.com ([212.159.85.26] helo=[192.168.7.2]) by mail.dcs.qmul.ac.uk with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.42) id 1CDJZ9-00064U-0A; Fri, 01 Oct 2004 10:19:04 +0100 Message-ID: <415D20EC.8080704@dcs.qmul.ac.uk> Date: Fri, 01 Oct 2004 10:18:36 +0100 From: Martin Berger User-Agent: Mozilla Thunderbird 0.6 (X11/20040519) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Hendrik Tews , caml-list@inria.fr Subject: Re: [Caml-list] Formal Methods References: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> In-Reply-To: Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-DCS-Interface-Port: 465 X-DCS-Auth-User: martinb X-DCS-clamav-result: clean (1CDJZ9-00064U-0A) X-DCS-uvscan-result: clean (1CDJZ9-00064U-0A) X-Miltered: at concorde with ID 415D2108.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 seldom:01 orders:97 identical:03 similarly:03 complicated:04 complicated:04 seems:05 seems:05 humans:05 practice:06 maybe:06 problem:07 attempted:07 programming:07 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > "Similarly, proving correctness of software using formal methods is > hopeless. > > This is just nonsense. You can prove the correctness of any piece > of software (provided it is correct). Its only some orders of > magnitute more expensive than developing the same software, > therefore proving correctness is seldom attempted in practice. it is a bit more complicated than that. it seems to be the case, and maybe that's what chaitin is getting at, that the more complicated the program under verification and the more complicated the property to be established, the more that verification is like writing a program. but then the question "is the specification correct?" becomes as hard as, or identical with "has the program that property?". so in the limit there seems to be a real problem in that we can trust verification only in as much as we can trust programming. BUT, and that's a very big "but", for many properties that happen to be of human interest, such as the absence of buffer-overflow errors, or the fact that a given program terminates, verification is often fairly easy to do and specification of the relevant property is easy. so easy in fact sometimes that it can be automatised. Sriram Rajamani for example, http://research.microsoft.com/~sriram/ has recently come up with some surprisingly powerful automatic verification tools. in summary, it seems that chaitin is right, but for properties and programs as simple as those humans care about, formal verification tends to be possible. martin ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners