3 ms·

> if we are limited by the halting problem for Turing machines? It's not how it works. Yes, there's no algorithm for solving the halting problem: given a rand

> if we are limited by the halting problem for Turing machines? It's not how it works. Yes, there's no algorithm for solving the halting problem: given a random program, prove that it halts. But we don't write programs by taking a random source code and trying to prove that it will halt. We create programs, and creating a provable halting program is easy. Just add executed instruction counter and halt the program when it equals some number. In other words: yes, there's at least one program you cannot prove whether it will halt or not, but it's irrelevant. You can always construct a program that halts.

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 algorithmverification 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]

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 algorithmverification 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]