5 ms·

You can have a condition that you need to be able to prove that some variable is strictly decreasing on each iteration. Then you ensure that the loop exits once

You can have a condition that you need to be able to prove that some variable is strictly decreasing on each iteration. Then you ensure that the loop exits once the variable reaches zero or less. ATS has this kind of proof built into the language, so that the type system helps you prove that a loop will always exit, and if it can't, it's a compile error. It's not entirely clear how useful this is in practice. While you may be able to prove that a loop always exits, it can prove nothing about how long it will take before it does. A loop never terminating, and one that terminates some time after the Milky Way has merged with Andromeda is pretty much equivalent from a practical standpoint.

chriswarbo 6y ago
From a computational perspective you're right, but for languages which allow formal verification (like ATS) there is a big difference between infinite loops and long-running loops. In particular, if we only care whether something exists then we can accept a long-running computation as proof without having to run it, whilst an infinite loop may be false. For example, a function which takes a list, an index and a proof that the index occurs in the list: we can look up the index safely, without having to care about the actual contents of the proof (the language ensures it's valid). On the other hand, we can write an infinite loop which claims to prove anything we like, but never actually has to cough up anything. For example: ProofOfRiemannConjecture myProof { while (true) {} }