Hacking away on this proof here. I'm really excited that I think I see all the machinery coming together. It's kind of strange, that there's this one argument that seems necessary that feels very... I don't know, mechanical, in the hazy-mathematical-analogy kind of way, that there are all of these requirements and hypotheses and inferences all buzzing around doing just the right things to each other, and yet, in the implementation, it translates to zero code. It feels so much, to my intuition, like the execution of a program, but it is just a pile of logical dominos that intstantaneously fall, and imply that the program can just go on its merry way and be sure that it is correct at a certain point.
Around 9ish arilinn borrowed lincoln3's PS2 since he's out of town, and then techstep, gopi, and I went out for taco bell and krispy kreme. Yum.
This means I still have 10 original glazed that need eating if any of y'all reading feel social and jonesing for sugar tomorrow.