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.

Rabbit without a hat

I've always been a bit annoyed when a mathematical result is pulled out, in the middle of a slick argument, because it works. Sometimes this presentation is necessary, since the long, painful path to the result is not useful in and of itself. Often, though, slickness hides the fact that mathematics is a lot of messy work.

An example of these is the closed form for F(n), the nth Fibonacci number. Without even getting in to the controversy of what qualifies as a closed form, this result has the "feature" that F(n) is equal to the sum of two roots of the quadratic r^2 = r + 1, after you multiply them by a suitable coefficient.

Certainly this result can be proved by induction: a nice exercise in simple induction. But how would you ever dream of coming up with the conjecture in the first place? This week I gave an account of how you might find your way from the recursive expression for F(n), and its closed form.