Prove it's correct

This topic always marks a sharp departure from hacker culture. On the one hand, when we're used to having fun implementing intuitive ideas in code, why would we divert ourselves into proving they do what we want? On the other hand, even if we wanted to, how can we prove that our code will always do the things we claim it will?

In spite of these nagging doubts, we began looking at proving recursive correctness --- suspiciously like induction (and so it should be). In order to be reasonable a piece of code performs as claimed, we have to examine each line of code in surprising detail. The pay-off is that unexpected "edge" cases sometimes become apparent when we're trying to prove the thing works.

I'm inclined to sing along with my students this week "October is sooo crazy." I think I've nearly gotten through the worse of my administrative (non-teaching) duties for a little while, and will come out the other side soon. Just one more departmental TA ad to post, and I'm almost there.