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