9 ms·

Could you give an example of where either is a problem in a practical program — one I’m likely to write as an SDE?

by FakeComments 8y ago

jcbrand 8y ago
Writing 100% bug-free smart contracts that can't be exploited by an adversary.
- FakeComments 8y ago
  Could you give an example of a practical contract which demonstrates this problem? My contention is that the overlap between useful smart contracts and ones which demonstrate those theoretical problems is basically nil.
  - anyfoo 8y ago
    Could you give me an example of a practical program (none of that "hello world" or "multiply two numbers"-grade stuff) that has entirely been proven correct, through tests or formal methods? Let's start with tests: If you don't write a test for every single possible case, you will not know if there is not an edge case in your program that you did not catch. Unfortunately, the number of cases for any program that isn't entirely trivial (and thus mostly useless) grows so enormously quickly that you simply cannot write an exhaustive amounts of tests. So instead, you have to classify your inputs and test "representative" inputs for each of those classes. However, to make the reasoning of what is a perfect classification, i.e. a classification where each input you give in your tests behaves the same (for a reasonable definition) as any other input in that class, requires proving non-trivial properties about the program. And that, the halting theorem tells us, is impossible as well. In simpler words: In even relatively simple programs, there are more tests to write than available lifetime, but theory also tells us that we can't know how to reduce the test cases to only the interesting ones.
rafiki6 8y ago
You will never be able to come up with all possible test cases to cover all possible scenarios. That's the idea. This applies to all practical programs. There is literally not a single piece of software that doesn't have a missed edge case in the world.
- FakeComments 8y ago
  Why not? Sure, you can’t in the general abstract case, but my exact point is that you can do this in practice, for programs which we actually write. Perhaps you could show an example of a useful program we can’t do that for? In my experience, it’s not due to either of those theoretical considerations that we don’t see it done — we just don’t see it done in practice for cost reasons.
  - troutwine 8y ago
    Sure. In Rust there's a function called [`str::repeat`](https://doc.rust-lang.org/std/primitive.str.html#method.repeat https://doc.rust-lang.org/std/primitive.str.html#method.repe...) that takes a string slice and repeats it a number of times, allocating a new String in the process. Do there exist inputs -- either string or repetitions -- for which the following function does not panic owing to allocation issues (as documented) but either 1. cause a SIGBART or similar to be thrown or 2. fail to produce a new string which is the correct multiple size of the original string slice? It's not possible, I contend, to answer this question with tests. The cardinality of input strings and repetitions is bounded but very, very high. You can for sure find _examples_ where `str::repeat` functions as documented but demonstrating that it always will is a different thing.
    - dooglius 8y ago
      GP is asking for cases where testing is demonstrably insufficient, not cases where you personally aren't convinced. If `str::repeat` is actually buggy for some inputs, in spite of testing, that would suffice as a counterexample.
      - 8y ago
anyfoo 8y ago
The halting problem generalizes to, roughly spoken, the fact that you cannot generally know what a program does (you might be able to tell for a specific program, but I can always give you a program where that fails). What this means in this context, for practical programs, ones you are "likely to write as an SDE", is that it is in general impossible to know in advance whether your program has bugs or not. So, the notion that a program can be proven bug free "if you write enough tests" is kinda funny for programs of even moderate complexity, ones that you are likely to write as an SDE. Aside: This "how does it matter in the real world" attitude reeks of anti-intellectualism and annoys me to no end. It does, you just don't know how.
- FakeComments 8y ago
  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.

Could you give an example of where either is a problem in a practical program — one I’m likely to write as an SDE?

jcbrand 8y ago

Writing 100% bug-free smart contracts that can't be exploited by an adversary.

FakeComments 8y ago
Could you give an example of a practical contract which demonstrates this problem? My contention is that the overlap between useful smart contracts and ones which demonstrate those theoretical problems is basically nil.
- anyfoo 8y ago
  Could you give me an example of a practical program (none of that "hello world" or "multiply two numbers"-grade stuff) that has entirely been proven correct, through tests or formal methods? Let's start with tests: If you don't write a test for every single possible case, you will not know if there is not an edge case in your program that you did not catch. Unfortunately, the number of cases for any program that isn't entirely trivial (and thus mostly useless) grows so enormously quickly that you simply cannot write an exhaustive amounts of tests. So instead, you have to classify your inputs and test "representative" inputs for each of those classes. However, to make the reasoning of what is a perfect classification, i.e. a classification where each input you give in your tests behaves the same (for a reasonable definition) as any other input in that class, requires proving non-trivial properties about the program. And that, the halting theorem tells us, is impossible as well. In simpler words: In even relatively simple programs, there are more tests to write than available lifetime, but theory also tells us that we can't know how to reduce the test cases to only the interesting ones.

rafiki6 8y ago

You will never be able to come up with all possible test cases to cover all possible scenarios. That's the idea. This applies to all practical programs. There is literally not a single piece of software that doesn't have a missed edge case in the world.

FakeComments 8y ago
Why not? Sure, you can’t in the general abstract case, but my exact point is that you can do this in practice, for programs which we actually write. Perhaps you could show an example of a useful program we can’t do that for? In my experience, it’s not due to either of those theoretical considerations that we don’t see it done — we just don’t see it done in practice for cost reasons.
- troutwine 8y ago
  Sure. In Rust there's a function called [`str::repeat`](https://doc.rust-lang.org/std/primitive.str.html#method.repeat https://doc.rust-lang.org/std/primitive.str.html#method.repe...) that takes a string slice and repeats it a number of times, allocating a new String in the process. Do there exist inputs -- either string or repetitions -- for which the following function does not panic owing to allocation issues (as documented) but either 1. cause a SIGBART or similar to be thrown or 2. fail to produce a new string which is the correct multiple size of the original string slice? It's not possible, I contend, to answer this question with tests. The cardinality of input strings and repetitions is bounded but very, very high. You can for sure find _examples_ where `str::repeat` functions as documented but demonstrating that it always will is a different thing.
  - dooglius 8y ago
    GP is asking for cases where testing is demonstrably insufficient, not cases where you personally aren't convinced. If `str::repeat` is actually buggy for some inputs, in spite of testing, that would suffice as a counterexample.
    - 8y ago

anyfoo 8y ago

The halting problem generalizes to, roughly spoken, the fact that you cannot generally know what a program does (you might be able to tell for a specific program, but I can always give you a program where that fails). What this means in this context, for practical programs, ones you are "likely to write as an SDE", is that it is in general impossible to know in advance whether your program has bugs or not. So, the notion that a program can be proven bug free "if you write enough tests" is kinda funny for programs of even moderate complexity, ones that you are likely to write as an SDE. Aside: This "how does it matter in the real world" attitude reeks of anti-intellectualism and annoys me to no end. It does, you just don't know how.

FakeComments 8y ago
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.