Three Dollar Quill

I had this whole neat idea about doing exploratory coding in marimo, and then verifying ideas using Dafny, but my initial attempts in this area have so far gone... not great.

Marimo is fine so far, but when I gave Dafny a recurrence relation and closed form for the optimal number of moves for a tower of Hanoi puzzle, I expected it to either get something à la "Even a computer could discover this", or to quickly bail out because I gave it almost nothing to work with. Instead it just... sat there, with no indication of what it was doing, or how long it would take.

Just checked, and it's at least possible for Dafny to successfully verify a file, so it's not obviously an issue that occurs every time.

After a little more poking, this does have something to do with the method specifically, but I'm, like, not sure what to do with that yet. I'll have to think about it, I guess.

...

Hold up, I searched the issues for some key words, found stuff that eventually led me to the experimental --disable-nonlinear-arithmetic flag. I pass it in, and...

Yay! It fails!

I needed it to commit to a course of action.

So, given that verification is failing, I think I need to write a lemma, and have it work via induction? I'll try to figure this out later. For now, I want to sleep.

Good night.