I'd tell you why
but I don't know
It's simple and
so complicated
I could walk all day
on the railroad tracks
but there's much more
to it than that
(from mirah's "sweepstakes prize")
Events of today include: got some writing work done, went to the ConCert reading group meeting and listened to people talk about Leroy's certif(ied/ying) C compiler, played some piano.
Also someone in the pre-ConCertRG chatter asked whether there were finite non-Boolean Heyting algebras. It took me a minute to dredge up the (positive) answer, and I added it to the Wikipedia page for Heyting algebras just for the hell of it. The short answer is that it's the lattice of open sets of the Sierpinski space.