[plt-scheme] Computers considered harmful

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