[Camllist] Formal Methods
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20040930 (17:34) 
From:  Jacques Carette <carette@m...> 
Subject:  RE: [Camllist] Formal Methods 
The same 'problem' occurs in symbolic computation: the zeroequivalence problem for constants is wellknown to be undecidable. However, in practice, constants that appear in real problems (ie ones that occur from physical models) are very easy to prove nonzero. The constants that are difficult to handle tend to arise in idealized settings. 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. 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. Consider the above as a metaobservation based on my experience, first as Sr. Architect at Maplesoft, now as a researcher applying formal methods to computer algebra. Jacques Original Message From: ownercamllist@pauillac.inria.fr [mailto:ownercamllist@pauillac.inria.fr] On Behalf Of David McClain Sent: September 30, 2004 11:51 AM To: camllist@inria.fr Subject: [Camllist] Formal Methods 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 nonspecialist 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)