October 27th, 2003

beartato phd

(no subject)

A series of recent breakthroughs on the research front. I have a crazy five-bullet-point definition of a certain property that can be enjoyed by a tuple of two contexts, a variable, a type and a substitution, a handful of lemmas that let me transfer knowledge of the property holding around in various ways, and one of the inductively maintained bullet points is exactly what I need for the big-mother soundness proof. I think. I hope.

Yesterday morning, neglected to mention went out to fuel & fuddle for tasty brunch with martin, tom7, sally, adam, pete. The service was slow as balls, though. Martin wanted to check out the renovated basement of the UC, so we did that. Played a game of DDR on the machine there. I still pretty much suck at it, but it's kinda fun. Tom7 drove adam, martin and I over to Paul's CDs. I picked up brubeck's "Time Out" because it caught my eye and I was appalled at myself for not owning it already. Went back home and played some other miscellaneous video games while waiting for ben to pick up martin.

The evening consisted mostly of work and talking to Donna about her work. Refinement types are a good deal more confusing than I thought.
beartato phd

(no subject)

So I am "virtually attending" this workshop thing going on between SRI, NASA langley, and here. I am a little depressed how little I understand of any of the talks. Part of the blame goes to the shoddy audio quality. It is very hard to hear what anyone is saying over the teleconferencing equipment.

Nonetheless Ricky Butler from Langley made some points about the difficulty of managing a large library of formal proofs that really resonated with me, specifically claiming that he thought good naming conventions for lemmas was of paramount importance. Now anyone that's managed to get me to talk about it knows that I have this tendency to rant that it's just fundamentally broken to do programming (and by extention, hacking up formal proofs) via text files that only know how to connect a reference to a function, say (or a lemma) to the definition of that function (or the proof of that lemma) via a single, fixed string of glyphs that the programmer has to agree on early, and type in every time she wants to use its referent.

I think I would be much happier living in an environment where I just create things which are functions or are lemmas, and live in some nice organized hierarchy incidentally, and have names incidentally. However, I might be totally misguided, and I might be massively overestimating the actual practical benefit of my blue-sky dreaming in this direction... when pressed to actually argue why structural editors in general are any good, I always seem to mumble and sputter.
beartato phd

(no subject)

Grading 354, listening to "Time Out". Nice album. Grading still sux0rz, however. At least people really nailed a few of the problems on this homework, though. One guy had a slick way of proving every function 2^n -> 2 is encodable via a polynomial over Z_2 over the variables x_1 ... x_n: Sort all possible input vectors lexicographically. Start with the polynomial 0. Go through all the possible input vectors. Say you're looking at b_1b_2...b_n. Check whether your polynomial gives the right answer. If it doesn't, just tweak it by adding the term x_1^(b_1)x_2^(b_2)...x_n^(b_n). This can't possibly fuck up any previous answer because you iterated over input vectors in lexicographic order; any previous vector has a zero in some position where the currect vector has a one. QED.
beartato phd

(no subject)

Gar. I have this premonition that, assuming I get through this whole grad school thing and fall into academia somewhere, I will totally adopt a Statman-esque course organization style, that is, minimal homework and tests and things that need to be actually graded.