[tom_mellior]

> > the existence of programs that might be "productive" in your sense, but might also never stop, and it is not possible to know in advance

> I struggle to imagine a practical case where we want to run a program that we didn't and couldn't know whether it worked though.

First-order theorem proving is a very practical case. Proof in first-order logic is "recursively enumerable", which means that we can write provers that, given a formula F, produce a proof of F in finite time if such a proof exists. But in general we don't know if a proof exists or how long it will take to find it. So if we start a prover, it will just sit there and not look "productive" until it either returns a proof or we kill it because we're tired of waiting.

[lmm]

But we wouldn't want to just leave such a theorem prover running indefinitely. Far more practical to have it check all possible proofs of length up to n (trivial to do in a total language), or at most run it for a particular number of days, months or years. At some point you do end the experiment.

[tom_mellior]

Sure. You usually run the prover with a timeout. The point is, this is a practical example of running a program where you cannot predict whether it will "work" or not. Additionally, when you reach the timeout, you will not have gained any information, i.e., the process is not "productive" in the sense discussed above.

Edit: Can't reply to your reply. Interesting. Yes, true, "there is no proof of length < N" is some information, but it's not information that tells you anything about the provability of your formula. It's not productive information. You can keep trying, but you won't be able to overturn the semidecidability of first-order logic in a Hacker News comment thread.

[lmm]

If the prover simply went into an infinite loop while checking the first proof candidate and never got as far as checking the second one, would it be working correctly? I would consider such a prover not useful, and a useful prover would be one that told me something when reaching the timeout, such as that there were no proofs for the given theorem shorter than a certain length.

[thamster]

This is handled in university CS algorithms courses. In such a case, dovetailing or interleaving the execution of the TM on the input would be used. Sipser pp. 150–152 https://courses.engr.illinois.edu/cs373/sp2009/lectures/old/...