## Comment Important Pedantic Correction (Score 1) 401

The test is based on an extension of Turing's halting problem in computer science. This states that there is no general way of knowing how an algorithm will finish, other than to run it.

This is **not** what it states, it states that there is no general way (=algorithm) of knowing whether any arbitrary algorithm will halt or not, given a specific input, other than to run it. If this were always true, one would not have theorem provers that work on code and generate a judgement about halting. Theorem provers about code exist. If it were always false, then theorem provers would be perfect and we'd be able to tell if code matched specification perfectly, which is not true either. The truth is in the middle, it works sometimes, i.e. not always. Since a theorem prover is an algorithm, and if one asked of it the halting property of an arbitrary piece of code, it may get caught in an infinite loop and be unable to answer. That does not preclude a general theorem prover from generating useful results on code about halting behavior (or any other behavior), it just can't answer every question about every piece of code, when given any possible input.

Omega = (\x.xx)(\x.xx)