March 15th, 2005

beartato phd

(no subject)

Oh hell yes. My proof-compression and -checking programs finally made it successfully through all 13074 declarations of the version of the TALT suite I've been using for testing. Previous to this last bugfix, it was only getting ~4000. SetCPUTimer tells me compression took about 2 hours, and the final typecheck took 30 seconds. Twelf takes about half an hour to check all the same stuff, but this is totally not a fair comparison, (to the 30s figure) because my tool doesn't do anything to correspond to mode-, termination-, or coverage-checking. Or parsing, for that matter! Nonetheless, it's a very promising number.
beartato phd

(no subject)

Coming back from dinner I decided to take the first plausible eastbound bus on fifth ave. to see how far it carried me towards home. This being because I'm not very familiar with the routes that go down fifth, and I figured I'd learn the same way I got familiar with the forbes routes back when I was a wee underclassman, i.e. mostly by just trying them. The 71C turns north on negley, apparently. Still gets me a good chunk of the way home if I'm in oakland, though.

I had the good fortune of bumping into iole200 just after I got off the bus, and was talked into paying a visit to lambdacalculus's house, since she was heading there to help make and eat dinner and watch yesterday's episode of "24". So I tagged along and actually managed to understand much of the "24" despite not being too familiar with this season's backstory. After that we watched a few episodes of "Arrested Development", which is also a pretty fucking brilliant show. I've mostly been out of the television loop since about sophomore year; it's good to know people are still making good new shows.

All this was on the amazing new projector device that tom and mike bought. Except for the weird effect of occasionally being able to catch just one RGB channel mid-eye-saccade, it was very nice watching everything bigger than life on the wall. It was something like 8' along the diagonal of the image.

Earlier today I had an advisor meeting, which went pretty well. In retrospect, this was probably due to me having results. In turn, careful thought suggests to me that this was because I did work during the last two weeks. I should be taking notes on this or something, I think. I don't want to jump the gun, but there may be some kind of causal relationship here.