[plt-scheme] Computers considered harmful

Use Dracula and demo that you can mechanize such proofs. -- Matthias




On May 7, 2009, at 11:33 AM, Stephen Bloch wrote:

>
> On May 7, 2009, at 9:51 AM, hendrik at topoi.pooq.com wrote:
>
>>> I think there's a serious illusion that formal verification and  
>>> careful
>>> thought can replace debugging.  Maybe someday, but not yet.
>>
>> And I'm sure debuging will never replace careful thought as a viable
>> methodology for anything that has to be reliable.
>
> As it happens, I was talking to my CS1 students just yesterday  
> about this exact issue.  How do you know a program is correct?  One  
> way is testing, which has the drawback that there are (generally)  
> infinitely many possible inputs, so you can't test them all.  The  
> other way is logic, which has the drawback that humans aren't very  
> good at it :-)  Anyway, we then went through a sorta-like-proof  
> that two different versions (one recursive, one iterative) of a  
> "count-matches" function work correctly.
>
>
> Stephen Bloch
> sbloch at adelphi.edu
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme