4 ms·

The problem with your reasoning is much like there being uncountably many real numbers: it turns out in practice, I only deal with a countable subset of computa

The problem with your reasoning is much like there being uncountably many real numbers: it turns out in practice, I only deal with a countable subset of computable numbers, and get by just fine doing so, and hence many results about “real numbers” don’t apply to my life. The mere existence of programs you can’t determine the halting status of doesn’t necessarily imply anything about the much, much smaller subset of programs we’d want to write for practical reasons — eg, managing my bank account. It’s also very strange to quote things like “if you write enough tests”, when in fact I didn’t say anything like that. Rather than address how a theoretical result connects to the real world, you assume without any thought that the kind of problematic cases which exist in theory actually relate to what we do in practice. Show me the actual connection, or admit the halting problem isn’t really a concern in practice: where in the course of my life as an SDE does it actually cause problems, because in my experience, I work in the subset of programs you can reason about. Many of the posters here make the same fundamental mistake: the existence of programs we can’t reason about doesn’t mean that there are no programs we can reason about — and in practice, we encounter the ones we can’t extremely rarely.

anyfoo 8y ago
> Show me the actual connection, or admit the halting problem isn’t really a concern in practice: where in the course of my life as an SDE does it actually cause problems, But were it not for the halting problem, we could automatically prove programs to be correct! So it affects you all the time: Because of the pesky halting problem, making sure that your program does what it should is really really hard instead of being plain automatic. I think the point you don't get is that the halting problem is not just "you cannot prove that a problem halts", it extends to "you cannot prove that a program does what it should do, period". And this is the reason why we need exhaustive tests on one side and elaborate verification methods on the other side, both still never giving 100% confidence. > because in my experience, I work in the subset of programs you can reason about. You can reason about them, but you cannot guarantee that they are bug-free. You ask me for a program "where the halting problem matters", and I say "pretty much any program you can find". On the contrary even, I ask you to provide me with a non-trivial program (i.e. one which is not just an academic exercise) that has been proven bug-free, through testing or other methods.
- anyfoo 8y ago
  I mean I don't even know what you are asking for when you say "show me a program where the halting problem matters"... Can I not just pick any program you (or anyone else) have not proven to be bug free? If you want a direct application of the halting problem itself, as in "does it terminate"... I don't know if my web browser finishes rendering all websites (even without JavaScript), so I guess I pick that?
- FakeComments 8y ago
  > were it not for the halting problem, we could automatically prove programs to be correct! But we actually can do this for a huge subset of programs — as long we we’re okay with false negatives, ie programs which are correct but that we can’t prove using our system. Precisely what I’m trying to call out is your mistake here: the existence of programs (in theory) which we can’t analyze (eg because of the halting problem) doesn’t imply anything at all about the programs we’re likely to encounter in practice. Those programs live in the subset of programs for which automatic reasoning does work. The correct interpretation of “it’s not possible to prove all programs” is “there exists some programs we can’t prove correctness of”, not “there are no programs we can prove the correctness of”. Show me that the programs we find useful overlap with the ones we can’t automatically prove — because in my experience, things like the halting problem are an abstract concern, and the programs we want to verify live solidly in the subset of programs we can automatically reason about. For any program we’re likely to encounter in practice, we’re in the subset of programs we can automatically prove correct, if we spent the effort to do so. (And I have done so before.)

anyfoo 8y ago

> Show me the actual connection, or admit the halting problem isn’t really a concern in practice: where in the course of my life as an SDE does it actually cause problems, But were it not for the halting problem, we could automatically prove programs to be correct! So it affects you all the time: Because of the pesky halting problem, making sure that your program does what it should is really really hard instead of being plain automatic. I think the point you don't get is that the halting problem is not just "you cannot prove that a problem halts", it extends to "you cannot prove that a program does what it should do, period". And this is the reason why we need exhaustive tests on one side and elaborate verification methods on the other side, both still never giving 100% confidence. > because in my experience, I work in the subset of programs you can reason about. You can reason about them, but you cannot guarantee that they are bug-free. You ask me for a program "where the halting problem matters", and I say "pretty much any program you can find". On the contrary even, I ask you to provide me with a non-trivial program (i.e. one which is not just an academic exercise) that has been proven bug-free, through testing or other methods.

anyfoo 8y ago
I mean I don't even know what you are asking for when you say "show me a program where the halting problem matters"... Can I not just pick any program you (or anyone else) have not proven to be bug free? If you want a direct application of the halting problem itself, as in "does it terminate"... I don't know if my web browser finishes rendering all websites (even without JavaScript), so I guess I pick that?
FakeComments 8y ago
> were it not for the halting problem, we could automatically prove programs to be correct! But we actually can do this for a huge subset of programs — as long we we’re okay with false negatives, ie programs which are correct but that we can’t prove using our system. Precisely what I’m trying to call out is your mistake here: the existence of programs (in theory) which we can’t analyze (eg because of the halting problem) doesn’t imply anything at all about the programs we’re likely to encounter in practice. Those programs live in the subset of programs for which automatic reasoning does work. The correct interpretation of “it’s not possible to prove all programs” is “there exists some programs we can’t prove correctness of”, not “there are no programs we can prove the correctness of”. Show me that the programs we find useful overlap with the ones we can’t automatically prove — because in my experience, things like the halting problem are an abstract concern, and the programs we want to verify live solidly in the subset of programs we can automatically reason about. For any program we’re likely to encounter in practice, we’re in the subset of programs we can automatically prove correct, if we spent the effort to do so. (And I have done so before.)