Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Programming Languages Going Above and Beyond. Parent comment
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
There are no comments on this comment yet.
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