Stewart: "Again, because we're on comedy central here, you may have to replace the word 'temerity' with 'balls'..."
Richard Clarke: "Government is just people. It's just people like you and me.
Stewart: "Oh, God, don't say that."
Wrote parsing, and in eXtreme pair-style with tom7, unification code with tom7 for the AUTOMATIC THEOREM PROVING BY WHICH I MEAN NOT AT ALL ADENOSINE TRIPHOSPHATE project. Earlier in the day went to a talk by Tom Hales, advisor of Sean McLaughlin, this guy that may be a grad student here at CMU in the fall. Neat things about the formalization of the Kepler Conjecture in HOL-Light. I have this feeling that this the stuff of mathematics history being made.
Went to the zebra lounge after the mad hacking spree with tom7. There found a quartet of cellos playing a terribly beautiful cover of the Goo Goo Dolls' "Iris" and some metallica song I didn't know. Talked with Kat (who had played with v and dave and I once) after they finished: sounds like I may be able to corner her friday and jam a bit. Played for a good hour or two on the piano after she had to leave. Had a surprisingly good time with "A-Train" and "I Will" and the Zelda overworld theme. That last one always gets a "hey, that's zelda!" out of some dork, if there are any dorks hanging around. In this case there was. And this other voice major totally randomly approached me for later jamming and stuff. And it looks like saturday night v (and hopefully also dave) are available. Oh, so much music. I'm looking forward to it.