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 RAA13310; Thu, 30 Sep 2004 17:51:29 +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 RAA12054 for ; Thu, 30 Sep 2004 17:51:28 +0200 (MET DST) Received: from plato.rocketdogcreative.com (plato.rocketdogcreative.com [66.139.78.99]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i8UFpRf7014989 for ; Thu, 30 Sep 2004 17:51:27 +0200 Received: from [10.0.1.3] (65-101-185-29.tcsn.qwest.net [65.101.185.29]) by plato.rocketdogcreative.com (8.11.6/8.11.6) with ESMTP id i8UFpPT26454 for ; Thu, 30 Sep 2004 08:51:26 -0700 Mime-Version: 1.0 (Apple Message framework v619) To: caml-list@inria.fr Message-Id: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> Content-Type: multipart/alternative; boundary=Apple-Mail-27-140684966 From: David McClain Subject: [Caml-list] Formal Methods Date: Thu, 30 Sep 2004 08:51:25 -0700 X-Mailer: Apple Mail (2.619) X-Miltered: at concorde with ID 415C2B7F.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; mcclain:01 mcclain:01 debugging:01 squares:01 fontfamily:01 debugging:01 squares:01 fontfamily:01 complexity:02 complexity:02 similarly:03 similarly:03 algorithms:03 algorithms:03 cautious:05 X-Attachments: type="text/enriched" Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk --Apple-Mail-27-140684966 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; format=flowed I have just been reviewing some papers by Greg Chaitin on Algorithmic Complexity Theory, in which he boldly states that "Similarly, proving correctness of software using formal methods is hopeless. Debugging is done experimentally, by trial and error. And cautious managers insist on running a new system in parallel with the old one until they believe that the new system works." from http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html He goes to great lengths to discuss the halting problem and its implications for proving correctness of algorithms. I wonder, as a non-specialist in this area, how the goals of FPL squares with this result? David McClain Senior Corporate Scientist Avisere, Inc. david.mcclain@avisere.com +1.520.390.7738 (USA) --Apple-Mail-27-140684966 Content-Transfer-Encoding: 7bit Content-Type: text/enriched; charset=US-ASCII I have just been reviewing some papers by Greg Chaitin on Algorithmic Complexity Theory, in which he boldly states that "TimesSimilarly, proving correctness of software using formal methods is hopeless. Debugging is done experimentally, by trial and error. And cautious managers insist on running a new system in parallel with the old one until they believe that the new system works." from http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html He goes to great lengths to discuss the halting problem and its implications for proving correctness of algorithms. I wonder, as a non-specialist in this area, how the goals of FPL squares with this result? David McClain Senior Corporate Scientist Avisere, Inc. david.mcclain@avisere.com +1.520.390.7738 (USA) --Apple-Mail-27-140684966-- ------------------- 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