January 14th, 2006

beartato phd

(no subject)

Over at Casa Del Beattie I ate some amazing spinach ravioli and meatballs prepared by mostly Mike and Sally with help from Sally's friend Diana, Diana's sister, and me. After that tried to catch this one guitarist over at the Quiet Storm with grammarnerd, but it turned out we were two hours late, so we listened to whoever it was that had come on stage by then for a little while (they were still pretty good) and played hangman. (highlights: "myopia", "ziggurat")

Despite almost total delinquency since coming back to pittsburgh (which I mentally justify by the fact that I put in quite a few nearly full days of work over break) I am still progressing quite rapidly towards having this Twelf proof of the correctness of Gödel's box-translation be really done and not just "essentially" done, which is the state it's been in for a week or so.
beartato phd

(no subject)

Finally got a decent night's sleep last night, perversely despite the fact that I stayed up kind of late doing pointless internet reading after getting back home from hanging out with grammarnerd. Woke up this morning with twelf on my mind and had a nice productive hacking session. Later on I discovered that I now get wireless from one of the first-floor lounges in Barco, and had dinner with Neal at Sam's, where we talked why the sort of multivariate calculus done in physics is one of the most insane* kinds of math.

*(a) I mean only "most insane" for a bad sort of insanity, and (b) really it is only insane in the way it is usually formulated. By (a) I certainly don't mean to ignore that there are lots of branches of math that are immensely more good-insane, and as for what to do about (b) I think calc could stand to be vastly less insane if it only expressed functions in a reasonable way, i.e. λ-notation for starters.