> the threshold where their halting-status is computable It's not a threshold in a strict sense. If a program is constructed from a proof (the Curry–Howard cor

> the threshold where their halting-status is computable It's not a threshold in a strict sense. If a program is constructed from a proof (the Curry–Howard correspondence), then it will provably halt regardless of its length or complexity. Most programs aren't constructed from formal proofs, of course, but a programmer always have some informal ideas why the program should work. We never take an arbitrary program and try to prove that it solves our problem. It is impossible anyway, if we aren't super-Turing (Rice's theorem). And if we want to prove that our program does what we need and fail to do that, we don't give up, but modify our program for it to be provable.