Jason (jcreed) wrote,

Today I had went to class, had a decent advisor meeting, and then I saw Karl talk about twelf encodings of the metatheory of singleton kinds (or, equally well, singleton types). I was struck by

  • 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.
Tags: books, math, social, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded