[Haskell-cafe] Proving correctness

Dominique Devriese dominique.devriese at cs.kuleuven.be
Fri Feb 11 17:09:05 CET 2011


Kashyap,

2011/2/11 C K Kashyap <ckkashyap at gmail.com>:
> I've come across this a few times - "In Haskell, once can prove the
> correctness of the code" - Is this true?
> I know that static typing and strong typing of Haskell eliminate a whole
> class of problems - is that related to the proving correctness?
> Is it about Quickcheck - if so, how is it different from having test sutites
> in projects using mainstream languages?

You may be confusing Haskell with dependently typed programming languages such
as Coq or Agda, where formal proofs of correctness properties of
programs can be verified by the type checker.

Dominique



More information about the Haskell-Cafe mailing list