Three Dollar Quill

Well, after spending longer than I'd like debugging my laptop—

I got back to copying tables over. On the one hand, it's almost done. On the other hand, exactly one of these last few pages secretly has a new, incomprehensible layout, and I need to psych myself up before I'm ready to either tweak my cleanup code again, or simply transcribe this one page.

So, putting that aside for now, I should get back to reading for Impliciula. One thing I need to put a pin in, even though I'm really curious about the tradeoffs, is how much expressive power I want to give the predicates in the refinement types. I really really really want to enable the pattern of "here is a simple implementation that is obviously correct, here is an optimized implementation, here is a proof that they give the same results on all inputs". (Okay, so technically it's better to prove it for given inputs without explicitly quantifying, because that's easier somehow. I think.) Looking over some of my own Dafny code, it looks like at least some of the stuff I want to prove doesn't need an excessive amount of power, unless I'm misreading things. (Also should allow things like "these related functions are specified with reference to each other's specifications, but their implementations are related differently, if at all.")

Anyway, time to wrap up, wind down, whatever.

Good night.