News for hackers. Stuff that matters.
Re:Ethereum is Doomed (2016) by FakeComments on Tuesday January 15, 2019 @02:21PM (#18914022)
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.

Re:Ethereum is Doomed (2016) by yongjik on Tuesday January 15, 2019 @03:02PM (#18914454)
When I was at grad school most of my research was about devising highly impractical (but kinda cute) algorithms for idealized machines with concurrent processes. These algorithms were usually about twenty lines long, but the correctness proof would span a dozen pages (and sometimes several hundred numbered equations) - at one point a reviewer got so disgusted that they called it "Proof by intimidation".

So, yeah, imagine doing that for any program with more than five hundred lines of code.

Re:Ethereum is Doomed (2016) by masklinn on Tuesday January 15, 2019 @04:10PM (#18915325)
> 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.

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.

Re:Ethereum is Doomed (2016) by lukifer on Tuesday January 15, 2019 @03:05PM (#18914492)
A computer is a state machine, with a number of potential states represented by 2^n (where n is the number of bits of storage/memory). As soon as n approaches some non-trivial number (which necessarily includes queued processor instructions, in addition to data!), the number of possible states rapidly exceeds the number of atoms in the known universe. There are simply too many permutations to test 100% of all cases for any program more complicated than "$x=2+2; assert($x==4);".

And that's just one constraint that makes the mythical "100% test coverage" practically infeasible. Another is: what tests the tests?

Re:Ethereum is Doomed (2016) by anyfoo on Tuesday January 15, 2019 @02:55PM (#18914374)
Well yeah, in practice we don't have Turing Machines with infinite bands, but finite memory, so the number of states is bounded.

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".

Re:Ethereum is Doomed (2016) by troutwine on Tuesday January 15, 2019 @02:45PM (#18914257)
Sure. In Rust there's a function called [`str::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.

Re:Ethereum is Doomed (2016) by dooglius on Tuesday January 15, 2019 @04:02PM (#18915209)
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.
Re:Ethereum is Doomed (2016) by troutwine on Tuesday January 15, 2019 @05:02PM (#18915896)
Ah, sure. What I'm trying to get at is discovering those inputs is the real trick. Comments elsewhere in this thread about exhaustive testing do a better job of getting at the same idea.
Re:Ethereum is Doomed (2016) by mimixco on Tuesday January 15, 2019 @02:50PM (#18914317)
The previous poster is correct. Software cannot be proven to be bug-free. This was considered axiomatic when I worked at IBM as a mainframe programmer on software that ran ATM machines, Social Security checks, etc.

You should definitely read up on the halting problem.

Re:Ethereum is Doomed (2016) by piano on Wednesday January 16, 2019 @05:36AM (#18919695)
> The previous poster is correct. Software cannot be proven to be bug-free.

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.

Re:Ethereum is Doomed (2016) by Izkata on Wednesday January 16, 2019 @11:31AM (#18922223)
The thing that's always bothered me about this argument is the translation between proof and code+underlying system. Bugs can still be introduced there. Certainly significantly fewer bugs in the final result, but I don't think I'd be confident in calling it proven 100% bug-free.
Re:Ethereum is Doomed (2016) by piano on Wednesday January 16, 2019 @01:00PM (#18923158)
In languages with termination analysis and dependent types, the source code _is_ the proof and it's verified by the compiler. Basically when such a program compiles, it's proved to be correct according to the specification.

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.

Re:Ethereum is Doomed (2016) by masklinn on Tuesday January 15, 2019 @04:57PM (#18915852)
Software can absolutely be proved bug free. By being proved. 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).
Re:Ethereum is Doomed (2016) by mimixco on Tuesday January 15, 2019 @09:22PM (#18917769)
You can't come up with enough tests to prove that software is bug-free. No program has ever been written which is bug-free.
Re:Ethereum is Doomed (2016) by masklinn on Wednesday January 16, 2019 @05:07AM (#18919576)
> You can't come up with enough tests to prove that software is bug-free.

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...

Re:Ethereum is Doomed (2016) by mimixco on Wednesday January 16, 2019 @09:09AM (#18920932)
I'm talking about real world software. It's unlikely that anyone cares if a Hello World program is bug-free.
Re:Ethereum is Doomed (2016) by masklinn on Wednesday January 16, 2019 @11:05AM (#18921974)
> I'm talking about real world software.

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?

Re:Ethereum is Doomed (2016) by mimixco on Wednesday January 16, 2019 @12:27PM (#18922777)
I did read it. I stick by my assertion. In practice, software cannot be proven to be bug free. This assertion has been borne out by numerous companies with nearly unlimited budgets who continue to find severe bugs in their software, despite extensive testing. While it's interesting academically that a single function could be tested and shown to be bug-free, it's not relevant in practice. It's the interaction of multiple functions and subsystems that leads to many bugs -- and inputs in edge cases lead to even more than that.
Re:Ethereum is Doomed (2016) by masklinn on Thursday January 17, 2019 @05:33AM (#18929737)
> I stick by my assertion. In practice, software cannot be proven to be bug free.

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).

Re:Ethereum is Doomed (2016) by piano on Wednesday January 16, 2019 @05:40AM (#18919712)
> 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.

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.

Re:Ethereum is Doomed (2016) by dooglius on Tuesday January 15, 2019 @04:11PM (#18915329)
SQLite had a vulnerability recently[0], despite being considered one of the most thoroughly tested projects out there. The reason why not is combinatorial explosion[1]: because complex software has so many possible inputs and states, it is not feasible for tests to cover every possible edge case.

[0] https://news.ycombinator.com/item?id=18685296

[1] https://en.wikipedia.org/wiki/Combinatorial_explosion