2 ms·
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
by 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) {}
}