Three Dollar Quill

Here we go, I've verified that my weird Dafny code appears to work, so I'm ready to talk about it.

The goal: Functions that return other functions which meaningfully depend on their outputs.

The problem: Dafny appears not to support creating closures. I tried the workaround of "make an object", and that ran into "can't allocate in functions" (which, from my basic experience with Rust, I guess makes sense (please note that Rust functions and Dafny functions are pretty different things)), but also "I tried returning a bound function from an instance, and that didn't seem to work, oh well".

The messed-up workaround: While Dafny, if I'm reading the grammar documentation correctly, doesn't have a way to declare a function inside a function, it does have the ability to use ensures clauses to describe what properties a function capable of doing such a thing would have, and then just, don't write a body for the function, and it will successfully reason about whatever currying-based nonsense you ask it to.

I suppose another possible approach would be to write a predicate describing the desired relationships, then using the predicate with an assignment statement to create a fake closure through Prolog Nonsense. I think that approach would be more flexible in some key ways, but I don't think I need them, so I'll keep on with what I'm doing now. And if I do end up needing the flexibility, I can write the predicate, replace the ensures clause with it, and move on.

...

All right, I've put together a few more of these helper functions. At this point, I'm just about ready to redo the absolute convergence predicates, knowing what I now know about how I want to set things up. I could try getting on with that now, or...

Or I could say "You know what, that's enough for now, I want a break from screens and to get ready for bed." Probably the smart play.

Good night.