11 Feb
2011
11 Feb
'11
11:09 a.m.
Kashyap,
2011/2/11 C K Kashyap
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