Don wrote: > I have to disagree with that. "Correctness proofs" are based on a total > fallacy. Attempting to proving that a program is correct (on a real > machine, as opposed to a theoretical one) is utterly ridiculous. > I'm genuinely astonished that such an absurd idea ever had any traction.
The idea isn't absurd, but you need to use it properly. Saying "I
have run a correctness prover on my code so there aren't any bugs"
is a fallacy, but so is "I have run unit tests with 100% coverage so
there aren't any bugs". The point of correctness proofs isn't that
they will find *all* the bugs, but rather that they will find a
completely different category of bugs than testing.
So you shouldn't run a correctness prover on your code to prove
that there aren't any bugs, but simply to find some of the bugs (and
you can find a lot of bugs with such a tool).
Jerome
--
mailto:jeber...@free.fr
http://jeberger.free.fr
Jabber: jeber...@jabber.fr
signature.asc
Description: OpenPGP digital signature
