Isn't this just the halting problem? Sure, for simple cases compiler could do it (in Java I guess my IDE will do it since the compiler doesn't care), but in the general case, how would a compiler figure this out?
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
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.
Yup, agreed