3 ms·
> The compiler still cannot tell when our loops will terminate (yes, this is possible). Isn't this just the halting problem? Sure, for simple cases compiler co
by looperhacks 3y ago
> The compiler still cannot tell when our loops will terminate (yes, this is possible).
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?
- two_handfuls 3y agoYes, 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
- benburton 3y agoThank you. I thought I was going crazy.
- IshKebab 3y agoIt 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.
- redjamjar 3y ago> The halting problem has almost no practical relevance because we don't really care about the general case. Yup, agreed