[Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008

[Dan Doel]

On Sunday 14 September 2008 6:59:06 am Rafael Almeida wrote:
> One thing have always bugged me: how do you prove that you have
> correctly proven something? I mean, when I write a code I'm formaly
> stating what I want to happen and bugs happen. If I try to prove some
> part of the code I write more formal text (which generally isn't even
> checked by a compiler); how can I be sure that my proof doesn't
> contain bugs? Why would it make my program less error-prone? Is there
> any article that tries to compare heavy testing with FM?

This isn't really a problem if you're programming in a language in which the 
proofs of program correctness are checked by the compiler/what have you, as 
Chaddaï has already said. In that case, it's similar to asking, "how do I know 
my Haskell programs are actually type correct?" Barring bugs in the tools 
(which, in the ideal case, are built on a simple enough foundation to be 
confidently proven correct by hand), it's not so much a concern.

A more difficult question is: how do I know that the formal specification I've 
written for my program is the right one? Tools can fairly easily check that 
your programs conform to a given specification, but they cannot (to my 
knowledge) check that your specification says exactly what you want it to say.

Of course, this is no worse than the case with test suites, since one can 
similarly ask, "how can I be sure the tests check for the properties/behavior 
that I actually want?"

-- Dan