[Haskell-cafe] Proving correctness

[Pavel Perikov]

Sorely, Haskell can't prove logic with it. No predicates on values, guarantee that proof is not _|_. Haskell makes bug free software affordable, that's true. But it's not a proof assistant.

pavel

On 14.02.2011, at 22:57, Albert Y. C. Lai wrote:

> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe