Could you give an example of where either is a problem in a practical program — one I’m likely to write as an SDE?
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.
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.
You should definitely read up on the halting problem.
Sure you can: you can prove software is correct through exhaustive testing. As noted previously it only works for small input space and simple programs (functions, really) but it does work, you can prove that a boolean xor is correct by enumerating its 4 inputs and checking that all of them produce the expected output.
This method can be applied to input spaces up to about 40 bits or so: https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
What an unexpected coincidence, so am I!
> It's unlikely that anyone cares if a Hello World program is bug-free.
Did you consider reading the link I provided at any point?
You can't "stick by your assertion" then provide something which has almost no relation to your original assertion, that's called "moving the goalposts".
This moving of goalposts is even more asinine when you're moving them exactly where the comment which you originally decried had put them.
Reminder: here is what you originally felt you needed to note was wrong:
> Software can not be proved bug-free by tests (and even that assertion is not completely true, you can prove software through exhaustive testing if it's very very simple).
Yes, it can, that's what the whole formally verified software branch is about. Of course, even with formally verified software, there can be failures caused by external factors such as faults in hardware etc. But some piece of software itself absolutely can be proved to be correct (ie. bug-free). It just takes special approaches such as programming languages amenable to formal proofs (eg. Idris).
Software is usually written in bug-inducing ways and using languages that hinder formal verification not because provably bug-free software is impossible but because it is typically too costly and difficult to write.
Of course this still leaves space for bugs outside the program itself which still may influence it, such as bugs in the operating system or firmware or the like. Which may be prevented by having a formally verified OS too :)
But even in such a case, there might still be hardware errors (electrical noise, for example). Which is why for example spacecrafts or critical industry machinery double or triple their whole architectures. In such case the formally verified software runs on eg. three instances simulatenously and these instances cross-check each other's results all the time. When a hardware fault occurs (a bit randomly flipped in memory for example), they find out they're not matching and re-calculate.
That's as close as you can get to zero bugs.
The number of possible inputs and states for even a moderately complex program is also so astronomically high that it quickly far surpasses the number of atoms that earth consists of, so, yeah, "cost reasons" is one way to put it. We also don't transform sheet rock into gold for "energy reasons".
So, yeah, imagine doing that for any program with more than five hundred lines of code.
And that's just one constraint that makes the mythical "100% test coverage" practically infeasible. Another is: what tests the tests?
No, you can not do that for programs which we actually write. Even just a trivial program taking an array of single-precision floats can't be exhaustively tested, there's north of 2^100 input states (assuming a 64b platform and arrays can't be bigger than that).
If a program on a 32b Windows system takes a file as input, that's like 2^10^15 possible input states…
We can test every single case for very simple, trivial programs e.g. we can exhaustively test a function with 32 bits of input (a 32-bit integer or a single-precision float: https://randomascii.wordpress.com/2014/01/27/theres-only-fou...) in a minute or so if the function is not too complex. It might be feasible to add a few more bits, but assuming the same trivial function at 40 bits you've jumped to ~4 hours, at 43 bits you need more than a day.
At 64 bits you need 8000 years.
Alternatively: let's say we want to exhaustively test 32 bits division. That's 64 bits of input * 26 cycles per division (we're optimistic) and let's say 4GHz, 2^64 * 2^4.7 / 2^31.9 = 119647558364 seconds, or about 3800 years.
And that's just the division itself, mind, we still need to account for some incrementing, jumping, etc…
And that's just to exhaustively test the division of two single-precision floats.
No, it can't be done with testing even for practical everyday programs, precisely because you never know how much your program is crossing into the "abstract general case" and which parts of it are more general than you think. Very often the cause of bugs is precisely this - that some part of a program behaves in a more general / less restricted way than the programmer thought.
It can be done with formal verification, but that's a whole another story.
Technically it's possible and is called "exhaustive testing", you can do it for fairly small input states e.g. you can test trig functions on all 32 bits inputs, that's only 4 billion values.
Non-trivial programs have way more state than that, consider a vector of f32, just the full vector (2^64 items) contains 2^96 possible states.
Any modern machine: https://randomascii.wordpress.com/2014/01/27/theres-only-fou...
It's the same order of magnitude as your CPU frequency, and trivially partitionable (and thus parallelisable), how fast exactly depends on the complexity of the function being tested, but assuming the entire thing happens in native code it's on the order of 1~10 minutes to go through all values, call both the FUT and the oracle and compare the results.
> Once states are added in, it quickly explodes beyond a simple 32-bit input space.
Then you're not testing a problem with a 32b input space anymore. My comment specifically points out that it's doable for small input states and gives 32 bits as an anchor at the upper end. If the program under test is fast enough and you're fine with hours-long tests you could get up to the low 40s and still be able to test every single value but since every bit doubles the number of states (and thus the time spent testing) it grows unreasonable extremely quickly.
> I know in my own work, we don't even bother.
Of course not, the average program is billions of orders of magnitude beyond 32 bits of input state. The current HN homepage is 42.5KB, that's ~350000 bits of input space. If you take an input file or some such you start stacking exponentials just so the number of bits in your input space doesn't get unwieldy.
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.
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.
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.
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?
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.)
My contention is that the overlap between useful smart contracts and ones which demonstrate those theoretical problems is basically nil.
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.