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.?)
 
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.
 
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. 
 
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
	
	
	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)