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