Yes, correct. The author is skipping something here.

The Dafny compiler only accepts programs if it can prove they terminate. You help it with a “decreases annotation”.

So it’s true that no every program provably terminates. But those programs that don’t will be rejected by the Dafny compiler.

In practice I suspect this is a good thing overall (writing your loops in such a way that it’s easy to prove they terminate is good style).

Official documentation: https://dafny.org/dafny/OnlineTutorial/Termination

Thank you. I thought I was going crazy.

It can't in the general case. When you're writing formally verified code (or hardware design) it is very common for the formal engine to just say "nope! couldn't prove it!".

But that doesn't mean it is useless. The halting problem has almost no practical relevance because we don't really care about the general case.

> The halting problem has almost no practical relevance because we don't really care about the general case.

Yup, agreed