February 25th, 2006

beartato phd

(no subject)

The weather is very nice today; Walnut Street is full of rich people, and of babies. I saw an oak leaf caught just so in an updrafting patch of breeze, so that it was rising almost imperceptibly, and spinning as slow as a lazy susan given a gentle turn. It stayed there, like it was fixed to the sky by an invisible, twisting piece of string, for a good two seconds before it jerked sideways and fell to the ground.
beartato phd

(no subject)

I went to this talk by Tom Hales yesterday — it wasn't all that noteworthy to me in particular since I had basically seen the same talk before, but the gist of it is that he takes very seriously the idea of mechanization of formal proofs in ordinary work-a-day mathematics, which is very cool. He started out as an "ordinary" mathematician working on the Kepler Conjecture. When his (partially computer-calculation-based) proof of the conjecture stalled for years in the journal peer-review process and eventually was merely "accepted" as being only as strong as experimental evidence because none of the reviewers actually felt capable of checking the correctness of his code, he set off on formalizing the whole damn thing.

Anyhow, it just reminded me of HOL-Light, the tool he uses to do his formalization in, and how simple it is supposed to be for having only a 1,000 loc "trusted computing base", that being a 1,000 line C program, I think. It got me wondering how much effort and code it would really take, comparatively, to hack up just a canonical-forms LF typechecker, a task whose easiness has long been a rule of thumb, and it turned out the thumb was right. About two hours of hacking, and 125 lines of ML. It even fits on one screen if I take out all the whitespace:


It's probably not very efficient at all, since I implemented contexts and signatures very naively, and it has a funny input syntax to make parsing relatively trivial. Still, proof of concept.
beartato phd

(no subject)

Glurgh, feeling as if I am sick now, but I'm not convinced I've actually caught anything. I'd slept in, shlumped about the house lethargically sittin' and programmin' until late-ish in the day, (with the exception of a brief excursion for lunch) and that kind of thing correlates well with me feeling all headeachey and crap-like. Shoulda done requisite laundry last night instead of putting it off 'till today and got up earlier got some fresh air. Now I've nothing left to do but regret my past missteps, and drown my sorrows in strawberry Pop-Tarts. The troubles I have seen, I tell you, nobody knows 'em.