I think one thing it means, is that, with the typesystem, you just can&#39;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&#39;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. <br>
<br>And it is correct only that far -- the value-level coding is still up to you, so no mind-reading...<br><br><br>--<br>Markus Läll<br><br><div class="gmail_quote">On Fri, Feb 11, 2011 at 1:16 PM, Ivan Lazar Miljenovic <span dir="ltr">&lt;<a href="mailto:ivan.miljenovic@gmail.com">ivan.miljenovic@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;"><div class="im">On 11 February 2011 22:06, C K Kashyap &lt;<a href="mailto:ckkashyap@gmail.com">ckkashyap@gmail.com</a>&gt; wrote:<br>

&gt; Hi Folks,<br>
&gt; I&#39;ve come across this a few times - &quot;In Haskell, once can prove the<br>
&gt; correctness of the code&quot; - Is this true?<br>
<br>
</div>I&#39;m not quite sure where you got that...<br>
<br>
But since Haskell is pure, we can also do equational reasoning, etc.<br>
to help prove correctness.  Admittedly, I don&#39;t know how many people<br>
actually do so...<br>
<div class="im"><br>
&gt; I know that static typing and strong typing of Haskell eliminate a whole<br>
&gt; class of problems - is that related to the proving correctness?<br>
&gt; Is it about Quickcheck - if so, how is it different from having test sutites<br>
&gt; in projects using mainstream languages?<br>
<br>
</div>QuickCheck doesn&#39;t prove correctness: I had a bug that survived<br>
several releases tested regularly during development with a QC-based<br>
testsuite before it arose (as it required a specific condition to be<br>
satisfied for the bug to happen).  As far as I know, a testsuite - no<br>
matter what language or what tools/methodologies are used - for a<br>
non-trivial piece of work just provides reasonable degree of assurance<br>
of correctness; after all, there could be a bug/problem you hadn&#39;t<br>
thought of!<br>
<br>
--<br>
Ivan Lazar Miljenovic<br>
<a href="mailto:Ivan.Miljenovic@gmail.com">Ivan.Miljenovic@gmail.com</a><br>
<a href="http://IvanMiljenovic.wordpress.com" target="_blank">IvanMiljenovic.wordpress.com</a><br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>