Coding 2024-01-17
I'm reading up on sums right now, and putting together plans for stuff to represent them in Python and Dafny. It's pretty straightforward to write Python code to evaluate concrete examples, but there are some wrinkles when it comes to writing stuff up in Dafny.
Stuff like:
- I don't know whether Dafny has a rational datatype
- A very very very quick skim of the Dafny documentation didn't reveal a way to define new semantics for existing operators... (And a slightly less quick skim indicates that this is explicitly not a thing you can do in Dafny.)
- So an equivalent of sigma notation that may involve rational functions of the index values would seem to require some kind of usage of "traits".
- Maybe it would make sense to write something that works in the integer domain to start with, and get some idea of the kinds of operations that I end up using?
Anyway, I'll hopefully finish skimming this chapter soon, and then go back to the beginning and read it more carefully. It's sort of interesting how trying to take an "implementation" perspective causes me to notice things that the text doesn't focus on. Like, if you're working with numbers mentally, going from the integers to the rationals is often not that big a deal (unless you're doing something with raising things to the powers of natural numbers, and that's the bit that gets changed). In software, that can be scary.
Anyway, I don't want to stay up any longer, so I'm going to wrap things up abruptly.
Good night.