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 TAA18538; Thu, 30 Sep 2004 19:34:07 +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 TAA16274 for ; Thu, 30 Sep 2004 19:34:06 +0200 (MET DST) Received: from cgpsrv2.cis.mcmaster.ca (univmail.CIS.McMaster.CA [130.113.64.46]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i8UHY4ZC029633 for ; Thu, 30 Sep 2004 19:34:05 +0200 Received: from [130.113.68.27] (account carette@univmail.cis.mcmaster.ca HELO pccarettej) by cgpsrv2.cis.mcmaster.ca (CommuniGate Pro SMTP 4.1.8) with ESMTP id 66940028; Thu, 30 Sep 2004 13:34:04 -0400 Reply-To: From: "Jacques Carette" To: "'David McClain'" , Subject: RE: [Caml-list] Formal Methods Date: Thu, 30 Sep 2004 13:35:44 -0400 Organization: McMaster University Message-ID: <003901c4a713$ea0e4f00$1b447182@cas.mcmaster.ca> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_NextPart_000_003A_01C4A6F2.62FCAF00" X-Priority: 3 (Normal) X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook, Build 10.0.6626 In-Reply-To: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1441 Importance: Normal X-Miltered: at concorde with ID 415C438D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; jacques:01 caml-list:01 'problem':01 constants:01 undecidable:01 constants:01 analogy:01 ocaml's:01 inference:01 degenerate:01 architect:99 jacques:01 mcclain:01 2004:99 caml-list:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk This is a multi-part message in MIME format. ------=_NextPart_000_003A_01C4A6F2.62FCAF00 Content-Type: text/plain; charset="US-ASCII" Content-Transfer-Encoding: quoted-printable The same 'problem' occurs in symbolic computation: the zero-equivalence problem for constants is well-known to be undecidable. However, in practice, constants that appear in real problems (ie ones that occur = from physical models) are very easy to prove non-zero. The constants that = are difficult to handle tend to arise in idealized settings. =20 Now that I have started also using Formal Methods for proving my code correct, I have encountered the same thing: most meaningful programs can = be proven correct (given the right tools), but I can also construct short = silly programs which none of the standard tools handle. =20 I also see an analogy with type systems such as Ocaml's: in theory, type inference is exponential, while in practice it is very fast. This is because the worst cases are very degenerate, and do not tend to occur in common / meaningful programs. =20 Consider the above as a meta-observation based on my experience, first = as Sr. Architect at Maplesoft, now as a researcher applying formal methods = to computer algebra. =20 Jacques =20 -----Original Message----- From: owner-caml-list@pauillac.inria.fr [mailto:owner-caml-list@pauillac.inria.fr] On Behalf Of David McClain Sent: September 30, 2004 11:51 AM To: caml-list@inria.fr Subject: [Caml-list] Formal Methods 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." from=20 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) ------=_NextPart_000_003A_01C4A6F2.62FCAF00 Content-Type: text/html; charset="US-ASCII" Content-Transfer-Encoding: quoted-printable Message
The=20 same 'problem' occurs in symbolic computation: the zero-equivalence = problem for=20 constants is well-known to be undecidable.  However, in practice, = constants=20 that appear in real problems (ie ones that occur from physical models) = are very=20 easy to prove non-zero.  The constants that are difficult to handle = tend to=20 arise in idealized settings.
 
Now=20 that I have started also using Formal Methods for proving my code = correct, I=20 have encountered the same thing: most meaningful programs can be proven = correct=20 (given the right tools), but I can also construct short silly programs = which=20 none of the standard tools handle.
 
I also=20 see an analogy with type systems such as Ocaml's: in theory, type = inference is=20 exponential, while in practice it is very fast.  This is because = the worst=20 cases are very degenerate, and do not tend to occur in common / = meaningful=20 programs.
 
Consider the above as a meta-observation based on my = experience, first as=20 Sr. Architect at Maplesoft, now as a researcher applying formal methods = to=20 computer algebra.
 
Jacques
 
-----Original Message-----
From:=20 owner-caml-list@pauillac.inria.fr = [mailto:owner-caml-list@pauillac.inria.fr]=20 On Behalf Of David McClain
Sent: September 30, 2004 = 11:51=20 AM
To: caml-list@inria.fr
Subject: [Caml-list] = Formal=20 Methods

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

"Similarly, = proving=20 correctness of software using formal methods is hopeless. Debugging is = done=20 experimentally, by trial and error. And cautious managers insist on = running a=20 new system in parallel with the old one until they believe that the = new system=20 works."

from=20 =

http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html

He = goes=20 to great lengths to discuss the halting problem and its implications = for=20 proving correctness of algorithms.

I wonder, as a = non-specialist in=20 this area, how the goals of FPL squares with this = result?

David McClain
Senior = Corporate Scientist
Avisere,=20 Inc.

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

------=_NextPart_000_003A_01C4A6F2.62FCAF00-- ------------------- 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