On Friday 11 February 2011 12:06:58, C K Kashyap wrote:
Hi Folks,
I've come across this a few times - "In Haskell, once can prove the correctness of the code" - Is this true?
One can also prove the correctness of the code in other languages. What makes these proofs much easier in Haskell than in many other languages is purity and immutability. Also the use of higher order combinators (you need prove foldr, map, ... correct only once, not everytime you use them). Thus, proving correctness of the code is feasible for more complicated programmes in Haskell than in many other languages. Nevertheless, for sufficiently complicated programmes, proving correctness is unfeasible in Haskell too.
I know that static typing and strong typing of Haskell eliminate a whole class of problems - is that related to the proving correctness?
Yes, strong static typing (and the free theorems mentioned by Steffen) give you a stronger foundation upon which to build the proof.
Is it about Quickcheck - if so, how is it different from having test sutites in projects using mainstream languages?
Testing can only prove code incorrect, it can never prove code correct (except for extremely simple cases where testing all possible inputs can be done; but guaranteeing that QuickCheck generates all possible inputs is generally harder than a proof without testing in those cases).