[Haskell-cafe] Proving correctness

[Dominique Devriese]

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