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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
