Coding 2024-06-20
I think Dafny has gotten some new capabilities since I last messed with it, which is nice. I'm still getting to grips with stuff like "how should the modules be laid out?", and I kind of feel like maybe I should try getting a fresh start on this code.
Quick notes on the organization, because I was spacing out thinking about something else, and it's late:
- There are functions that are good for reasoning about sums.
- There are functions that are good for reasoning about those functions.
- There are methods that relate those functions to actual code.
- There are lemmas that allow the implementation of the method, and lemmas required to relate the method to the function.
It's probably safe to not try too hard to surface the lemmas, but I'm not sure how best to lay out everything else. I'll have to think about this some more. (I was thinking about Dafny stuff earlier, but it was mostly about a more sensible approach to the higher-order function ideas I had earlier.)
Anyway, that's all I've got for now.
Good night.