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 ann

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 https://dafny.org/dafny/OnlineTutorial/Termination