Three Dollar Quill

Dafny is a land of contrasts.

I'm getting code ported over, and being careful about where to put it, and working to make it less brittle, but unfortunately... Sometimes changes that I think will make the code less brittle, or at least easier to understand, make it more brittle, which is unfortunate. And it turns out that some of these extra diagnostics increase the resource usage and the variance, so I can't really use them unless I figure out how to tune the code even harder. And it's not even always obvious which code will be brittle.

How it's all shaken out is, I've gotten my finite sum code to parity with the original version, but I'm feeling some aesthetic quibbles, so I'm going to try to polish this some more tomorrow. Then I can work on some of the more interesting ideas I wrote down over the past week.

Anyway, I'd like to get some sleep now.

Good night.