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 TAA18040; Thu, 30 Sep 2004 19:20:14 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA13161 for ; Thu, 30 Sep 2004 19:20:12 +0200 (MET DST) Received: from orsfmr001.jf.intel.com (fmr12.intel.com [134.134.136.15]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i8UHKBDK013730 for ; Thu, 30 Sep 2004 19:20:12 +0200 Received: from talaria.jf.intel.com (talaria.jf.intel.com [10.7.209.7]) by orsfmr001.jf.intel.com (8.12.9-20030918-01/8.12.9/d: major-outer.mc,v 1.15 2004/01/30 18:16:28 root Exp $) with ESMTP id i8UHKA4U020827; Thu, 30 Sep 2004 17:20:10 GMT Received: from orsmsxvs040.jf.intel.com (orsmsxvs040.jf.intel.com [192.168.65.206]) by talaria.jf.intel.com (8.12.9-20030918-01/8.12.9/d: major-inner.mc,v 1.11 2004/07/29 22:51:53 root Exp $) with SMTP id i8UHBUXC025963; Thu, 30 Sep 2004 17:11:39 GMT Received: from orsmsx331.amr.corp.intel.com ([192.168.65.56]) by orsmsxvs040.jf.intel.com (SAVSMTP 3.1.2.35) with SMTP id M2004093010195312318 ; Thu, 30 Sep 2004 10:19:53 -0700 Received: from orsmsx407.amr.corp.intel.com ([192.168.65.50]) by orsmsx331.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.0); Thu, 30 Sep 2004 10:19:51 -0700 X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----_=_NextPart_001_01C4A711.B16E6AA5" Subject: RE: [Caml-list] Formal Methods Date: Thu, 30 Sep 2004 10:19:50 -0700 Message-ID: <012676D607FCF54E986746512C22CE7D0FE7AC@orsmsx407> Thread-Topic: [Caml-list] Formal Methods Thread-Index: AcSnBfm+2Un509bKTLm8Xuxja83IKwAB+39g From: "Harrison, John R" To: "David McClain" Cc: "Harrison, John R" , X-OriginalArrivalTime: 30 Sep 2004 17:19:51.0721 (UTC) FILETIME=[B214D990:01C4A711] X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang) X-Miltered: at nez-perce with ID 415C404B.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 johnh:01 provers:01 robbins:99 conjecture:01 real-world:01 niches:01 mcclain:01 2004:99 caml-list:01 debugging:01 squares:01 mcclain:01 provers:01 robbins:99 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk This is a multi-part message in MIME format. ------_=_NextPart_001_01C4A711.B16E6AA5 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable When he says that "theorem proving algorithms do not work [...] they only prove trivial theorems", he may just be out of date, or he may only be talking about completely automatic provers. (Even then his claim is a bit questionable: what about the Robbins Conjecture etc.?) =20 I didn't notice anything about the relevance of the halting problem in that page, so maybe it's somewhere else. Anyway, it's clearly not relevant to proving the correctness of typical real-world algorithms, whatever he may or may not say. =20 His general dismissive attitude to formal methods is not uncommon. And it's prefectly reasonable to point out that modern computer systems can be so complex and ill-defined that they are hardly amenable to formal treatment. But a more balanced view would acknowledge the significant success of formal methods in certain niches, and their role in trying to check that very unmastered complexity.=20 =20 John. -----Original Message----- From: owner-caml-list@pauillac.inria.fr [mailto:owner-caml-list@pauillac.inria.fr] On Behalf Of David McClain Sent: Thursday, September 30, 2004 8:51 AM To: caml-list@inria.fr Subject: [Caml-list] Formal Methods =09 =09 I have just been reviewing some papers by Greg Chaitin on Algorithmic Complexity Theory, in which he boldly states that=20 "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."=20 from=20 http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html=20 He goes to great lengths to discuss the halting problem and its implications for proving correctness of algorithms.=20 I wonder, as a non-specialist in this area, how the goals of FPL squares with this result?=20 David McClain=20 Senior Corporate Scientist=20 Avisere, Inc.=20 david.mcclain@avisere.com=20 +1.520.390.7738 (USA)=20 ------_=_NextPart_001_01C4A711.B16E6AA5 Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Message
When=20 he says that "theorem proving algorithms do not work [...] they only = prove=20 trivial theorems",
he may=20 just be out of date, or he may only be talking = about completely=20 automatic provers. (Even
then=20 his claim is a bit questionable: what about the Robbins Conjecture=20 etc.?)
 
I=20 didn't notice anything about the relevance of the halting = problem in=20 that page, so maybe it's
somewhere else. Anyway, it's clearly not relevant to proving = the=20 correctness of typical real-world
algorithms, whatever he may or may not = say.
 
His=20 general dismissive attitude to formal methods is not uncommon. And it's=20 prefectly reasonable
to=20 point out that modern computer systems can be so complex and=20 ill-defined that they are hardly
amenable to formal treatment. But a more balanced view would = acknowledge=20 the significant
success of formal methods in certain niches, = and their role=20 in trying to check that very = unmastered
complexity.
 
John.
-----Original Message-----
From:=20 owner-caml-list@pauillac.inria.fr = [mailto:owner-caml-list@pauillac.inria.fr]=20 On Behalf Of David McClain
Sent: Thursday, September = 30, 2004=20 8:51 AM
To: caml-list@inria.fr
Subject: = [Caml-list] Formal=20 Methods

I have just been reviewing some papers by Greg Chaitin on = Algorithmic=20 Complexity Theory, in which he boldly states that

"Similarly, proving correctness of = software=20 using formal methods is hopeless. Debugging is done experimentally, by = trial=20 and error. And cautious managers insist on running a new system in = parallel=20 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=20 implications for proving correctness of algorithms.

I wonder, as a non-specialist in this area, how the goals of FPL = squares=20 with this result?
David McClain
Senior Corporate Scientist
Avisere, Inc.

david.mcclain@avisere.com
+1.520.390.7738 (USA)

------_=_NextPart_001_01C4A711.B16E6AA5-- ------------------- 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