- how beautiful the underlying theory of singletons is
- again how powerful a tool hereditary canonicalization is
- how much I prefer spine form (i.e. focusing) presentations of LF to the apparently popular approach of considering non-fully-applied atomic terms
- how gross and write-only twelf concrete syntax tends to be. I think the only reason I can read my own code is that it is my own code, and I know it backwards and forwards already. Karl's stuff seems pretty well written as twelf code goes, but it's still a lot harder to slog through it in a talk than, like, pseudocode of an ordinary program in an ordinary programming language. Not really a fair comparison, but still.
Later read some more of Bloom, still wading through the Whitman chapter. Even though sometimes it feels like Bloom's opinion of you is 90% determined by whether you are a fan of (or in fact are one of) the select club of writers he deifies, and only like 10% by the quality of your work, he is quite a decent writer himself. I've enjoyed reading many paragraphs I violently disagree with by content, because they are so nicely written. I could listen to him mumble all day about his Anxiety of Influence, his "the American Religion", his Creative Misprision.
In the evening I was torn between going to D's and hanging out at martinivixen'n'mistergone's where they were watching the steelers season opener. Decided for the latter, mostly because I didn't feel in a noisy-bar mood. I think I kinda understood most of the football game, but the main lesson of the evening is that sk4p and mistergone are pee-your-pants funny when they get going.