Three Dollar Quill

All right. Skimmed to the end of the Sums chapter, and now it's time to look at it again, more carefully.

I'm currently sort of vacillating between "in Dafny, just go all in on doing arithmetic with real values" (and hope there aren't precision issues when it comes to doing purely verification), and "okay, but the chapter mentioned complex numbers, so I should really try to define traits to support algebras" (I have no experience writing traits in Dafny).

The reasonable course of action is to see how far I can get with "a data type that includes integral bounds, optional predicates, and a function from integers to reals". It's been really easy for me to get caught up in thinking about stuff like "Oh, this operator is basically a predicate followed by and in Python", and lose sight of the fact that it's just as important, if not moreso, to have tools for manipulating these forms, and not just evaluating them.

It's way too late to mess around with code right now, but here's the main question I think I'd like to address:

Given some format for expressing an infinite sum, is it possible to express the predicate "this sum converges absolutely"? Furthermore, can I properly express the implications of that for reasoning? If I can't figure out how to do that, then it's probably not worth trying to manipulate the sums programmatically.

We'll see where I get with that in a few days, hopefully. For now, it's later than I meant to be writing this.

Good night.