[Haskell-cafe] Proving correctness
Pavel Perikov
perikov at gmail.com
Mon Feb 14 21:03:26 CET 2011
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
More information about the Haskell-Cafe
mailing list