3 ms·
To some extent you are correct, but I think you are over-egging your point. It is, of course, trivially possible to construct a program that halts. Or even to
by sago 7y ago
To some extent you are correct, but I think you are over-egging your point.
It is, of course, trivially possible to construct a program that halts. Or even to modify an arbitrary program to make it halt (a good debugging tactic when things seem to be running awry). But the programs we write on a daily basis are routinely much more complicated than the threshold where their halting-status is computable.
I agree that we often intend to write programs that are guaranteed to halt. And generally code with some informal heuristic logic as to why our code probably will. But you don't have to do a lot of futzing around with formal methods and algorithm verification to know how loose that reasoning can be.
- red75prime 7y ago> 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.
- deleted 7y ago[deleted]