Re: [Haskell-cafe] Proving correctness

I think one thing it means, is that, with the typesystem, you just can't do random things where-ever you want. Like, in the pure world if you want to transform values from one type to another, you always need to have implementations of functions available to do that. (You can't just take a pure value, get its mem location and interpret it as something else, without being explicid about it.) So when lining up your code (composing functions), you can be sure, that at least as far as types are concerned, everything is correct -- that such a program, that you wrote, can actually exist == that all the apropriate functions exist. And it is correct only that far -- the value-level coding is still up to you, so no mind-reading... -- Markus Läll On Fri, Feb 11, 2011 at 1:16 PM, Ivan Lazar Miljenovic < ivan.miljenovic@gmail.com> wrote:

On 11 February 2011 22: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'm not quite sure where you got that...

But since Haskell is pure, we can also do equational reasoning, etc. to help prove correctness. Admittedly, I don't know how many people actually do so...

...

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?

QuickCheck doesn't prove correctness: I had a bug that survived several releases tested regularly during development with a QC-based testsuite before it arose (as it required a specific condition to be satisfied for the bug to happen). As far as I know, a testsuite - no matter what language or what tools/methodologies are used - for a non-trivial piece of work just provides reasonable degree of assurance of correctness; after all, there could be a bug/problem you hadn't thought of!

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com IvanMiljenovic.wordpress.com

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe