<div dir="ltr">I'm not replying to you nor<span style="font-family:arial,sans-serif;font-size:13px"> Michael Orlitzky</span>. <div>I'm replying to Richard A. O'Keefe.</div><div><br></div><div>You can see that by looking at which message was quoted below my actual response.</div>
<div>I hope it will make things clearer, because I'm actually not arguing at all against what you are saying :-)</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On 26 June 2014 13:44, Erik Hesselink <span dir="ltr"><<a href="mailto:hesselink@gmail.com" target="_blank">hesselink@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On Thu, Jun 26, 2014 at 2:24 PM, Bob Hutchison <<a href="mailto:hutch-lists@recursive.ca">hutch-lists@recursive.ca</a>> wrote:<br>

><br>
> On Jun 26, 2014, at 3:10 AM, Erik Hesselink <<a href="mailto:hesselink@gmail.com">hesselink@gmail.com</a>> wrote:<br>
><br>
>> On Wed, Jun 25, 2014 at 5:47 PM, Michael Orlitzky <<a href="mailto:michael@orlitzky.com">michael@orlitzky.com</a>> wrote:<br>
>>> On 06/25/2014 11:24 AM, Francesco Ariis wrote:<br>
>>>> On Wed, Jun 25, 2014 at 02:45:37PM +0200, Mateusz Kowalczyk wrote:<br>
>>>>> While I disagree with initial view that testing is useless, I certainly<br>
>>>>> disagree with this approach too. There are plenty proof-assistants using<br>
>>>>> type-checking to prove programs correct. That's not to say Haskell<br>
>>>>> itself is suited for such task. If you have a type system strong enough,<br>
>>>>> classical tests are no longer required because you can encode all the<br>
>>>>> properties you need in types proving at compile time that your program<br>
>>>>> is in fact correct.<br>
>>>>><br>
>>>><br>
>>>> For non-believers, here is a blog post that opened my eyes on the matter [1].<br>
>>>><br>
>>>> [1] <a href="http://lambda.jstolarek.com/2013/12/data-is-evidence/" target="_blank">http://lambda.jstolarek.com/2013/12/data-is-evidence/</a><br>
>>><br>
>>> None of that helps if you write the wrong program. Your program may<br>
>>> typecheck, but if you're expecting "42" as output and your program hums<br>
>>> the Star Trek theme instead, the fact that it correctly does the wrong<br>
>>> thing won't be much consolation.<br>
>><br>
>> The same goes for any kind of testing, though. All these (writing the<br>
>> program, giving types for the program and testing the program) are<br>
>> different ways of specifying the same thing. The benefit from doing it<br>
>> twice in different ways, is that it's unlikely that you'll do it wrong<br>
>> twice *in the same way*.<br>
><br>
> So, tell me about QuickCheck… why is this thing thought so highly of? (this is a rhetorical question, I don’t need an answer :-)<br>
><br>
> The problem isn’t really the unexpected humming of a song. It’s answering 43 when you’re expecting 42.<br>
<br>
</div></div>Are you replying to me, or Michael Orlitzky? Because I'm not sure what<br>
point you're making. I'm not arguing against the use of tests *or*<br>
types. I'm just saying neither is going to give you complete<br>
guarantees, but using either one is already much better than using<br>
none.<br>
<div class="HOEnZb"><div class="h5"><br>
Erik<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>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div dir="ltr"><div><b>A\ois</b></div><div><div><a href="http://twitter.com/aloiscochard" target="_blank">http://twitter.com/aloiscochard</a></div>
<div><a href="http://github.com/aloiscochard" target="_blank">http://github.com/aloiscochard</a></div></div></div>
</div>