I did some work years ago about giving a predicate logic treatment of Haskell, based on earlier work for Miranda, and formalised some proofs based on this in Isabelle. Here are the links: Logic for Miranda, revisited [from Formal Aspects of Computing, 1995] http://www.cs.kent.ac.uk/pubs/1995/63/index.html Formulating Haskell [from Functional Programming, Glasgow 1992] http://www.cs.kent.ac.uk/pubs/1992/123/index.html Miranda in Isabelle (with Steve Hill) [from Isabelle Workshop, 1995] http://www.cs.kent.ac.uk/pubs/1995/209/index.html Regards, Simon On 11 Feb 2011, at 11:06, 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?
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?
Regards, Kashyap _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe