Had a fun discussion/twelf hacking session with lambdacalculus. It was like watching an action movie with constant and harrowing dangers at every turn but ultimately a happy ending. Except that giving the hero suggestions actually resulted in a greater chance of success. And the hero was a program. A program that is an implementation of a dependent type theory. Which, I admit, is not the typical setup of your average hollywood summer-blockbuster explosion-fest. But I would so watch that movie.
The third paragraph of this page is a thing of beauty. The way it ends perfectly sums up the contradiction between the need to be hard on oneself to some degree to get better at anything, and on the other hand the drive to actually enjoy being good at it.