[Haskell-cafe] Proving correctness

[Albert Y. C. Lai]

On 11-02-12 09:40 PM, Brandon S Allbery KF8NH wrote:
> Only up to a point.  While most of the responses so far focus on the
> question from one direction, the other is epitomized by a Knuth quote:
>
> "Beware of bugs in the above code; I have only proved it correct, not tried it."

Knuth's definition of "proof" is of the sketchy kind of the mathematics 
community, not remotely close to the Coq kind. Even Dijsktra's and 
Bird's kind offers higher assurance than the traditional mathematician's 
sketchy kind.

There are still gaps, but drastically narrower than Knuth's gaps, and 
bridgeable with probability arbitrarily close to 1:

Possible defects in theorem provers: Use several theorem provers and/or 
several independent alternative implementations (both alternative 
software and alternative hardware).

Possible deviation of Haskell compilers from your assumed formal 
semantics of Haskell: Verify the compilers too, or modify the compilers 
to emit some sort of proof-carrying code.

Possible defects in target hardware: The hardware people are way ahead 
in improving both formal verification and manufacturing processes to 
reduce defects.

When John Harrison ( http://www.cl.cam.ac.uk/~jrh13/ ) has a proof for a 
floating-point algorithm, I would not dare to apply the Knuth quote on it.