Re: [Caml-list] Programming with correctness guarantees

[skaller <skaller@users.sourceforge.net>]

On Thu, 2007-02-01 at 21:57 +0100, Jean-Christophe Filliatre wrote:

> This is a statement easily established by most automatic provers. Then
> there is no need testing function min anymore, since it has been
> proved correct for _any_ input values.

This isn't right, IMHO: there is still need to test: 
after all the proof itself, and the theorem prover,
the operating system, etc, all introduce additional risks.

The point is that you no longer rely solely on the WORST
possible way of guessing if a program is going to work: testing.
Instead you rely on BOTH proof and testing, and you can put
a lot more effort (money) into the proof than the testing
to get the best results. But you never forget to actually test
the code too!

Don't forget that even with perfect machine model .. the actual
specification may be wrong! Correctness isn't enough! The program
has to actually work! But now, you can more easily blame the
spec writer than the programmer if it doesn't ... :)

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net