Hacker News Reader

Comment by this_user | Hacker News Reader

The issue with smart contracts is that the people behind the idea don't seem to understand that the issue with traditional contracts does not lie in the parts that a clearly defined, but in those that are not. These are the parts where the legal system comes into play in order to reach a decision on grey areas like that.

The other problem is the obvious issue that smart contracts make the implicit assumption that we are able to write bug-free code. Evidently, that is not the case.

There clearly needs to be some sort of mechanism to sort out issues that may arise from this. But in practice Ethereum has replaced an imperfect but robust mechanism in the form of the legal system with one guy, who is accountable to no one, making discretionary decisions with no guidelines to bind him.

View on HN

IMO the major shortcoming of smart contracts is that they have no tie to the real world, so the only thing they can really govern is other contracts, which themselves can only do the same thing. They can't be very interesting without oracles (e.g. Augur).

so is Augur an oracle that makes smart contracts interesting again? MakerDAO uses an oracle for the ETH/USD price as part of is DAI system for creating a decentralised $-pegged token. It seems like there are ways to solve the issue of getting real world information into Ethereum.

Yeah, but the point is sort of that the interesting ones are not simply "code is law," since there is an element of trust involved in them. They're code + human oracles.

And grey areas are useful to society, they allow some imprecisions.

It's not a bug, it's a feature!

The second the code someone wrote cost the developers money, suddenly the code wasn’t the contract any more.

The platform has more far reaching use-cases than being used to replace legal contracts, and written contracts can have "bugs" just as smart contracts can.

Do these far reaching use-cases matter in practice?

> ... written contracts can have "bugs" just as smart contracts can.

The onus on smart contracts is to come up with use cases where they are superior to written contract, not to find examples where they are equally flawed.

The purpose is to remove the middleman to have an autonomous outcome and by that they have succeeded. However, just as contracts have evolved over time after iterations have been found to have "bugs", I'm sure these will as well.

It does not cut out middlemen it only renames them to "oracle".

Right, but the bugs in written contracts can be negotiated in litigation

Litigation can be an asset or a liability depending on which way it goes for you, of course. Double edged sword for sure.

Smart contracts should not be compared with traditional contracts. They have very little to do with each other and it's an unfortunate name that even Vitalik himself regrets. They are just persistent scripts that run in parallell on a decentralised network. Using them for legal systems is a very niche use case.

Yeah, this. They can be used to replace some legal agreements. They can be used as a replacement for escrow. But that is a small slice of the capabilities of smart contracts.

I don't know why this is downvoted, it's completely accurate. Source: [0]

[0]: twitter.com/vitalikbuterin/status/1051160932699770882

It's downvoted because blockchains are evil

The benefit, transparent provably fair open source code that can automate financial transactions outweighs these issues. I don't think smart contracts on Ethereum not being fully autonomous and fully decentralized is a huge issue to normal consumers that might interact with them.

Old Thing does W, X and Y imperfectly.

New Thing does W and Z imperfectly.

Therefore, New Thing is doomed.

This analogy doesn't tell us anything useful. It is not a logical certainty that W, X and Y render the need for W and Z useless, but it's certainly logically permissible depending on the actual values of the variables.

More like...

Old thing does W imperfectly.

New thing does X. Proponents claim that X solves W's imperfections.

Turns out that it doesn't. Opponents claim that X hasn't much value then, so it's doomed.

Smart contracts does things like "if you replay old transactions on me I get my money back", or "you receive the corresposing private key to this public key if and only if you sign this transaction".

Clearly the use case is in bypassing a third parties and avoiding risk. There is no clear value in grey areas there. In valuing technology, it is the best use case you can think of that counts, not the worst.

Ethereum is a specific form of smart contracts where the use case compared to other forms is perhaps not as clear cut, but that doesn't stop people from speculating on the possibility.

It did spark some research into formally verifiable code so not all hope is lost; also other interesting spin-offs like zero-knowledge proofs in cryptography etc. are all very interesting. Now that the hype on speculation is gone, we can hope there’ll be more interesting “blockchain” news about moving research in this area forward, without recently seen nonsense.

If you write enough tests you could probably know for a fact that your contract doesn't have any bugs.

Tests can only prove the presence of bugs, not their absence.

You should probably read up on axiomatic incompleteness and the halting problem.

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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

I'm talking about real world software. It's unlikely that anyone cares if a Hello World program is bug-free.

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

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.

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

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

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.

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.

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

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.

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?

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

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

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

> You will never be able to come up with all possible test cases to cover all possible scenarios.

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.

Not sure what machine can possibly completely test a problem with a 32-bit input space in any "practical" or "reasonable" time. Once states are added in, it quickly explodes beyond a simple 32-bit input space. I have yet to see any literature showing that "Exhaustive" testing is even marginally feasible. I know in my own work, we don't even bother. We come up with the test cases we can and leave the rest to the Software gods.

> Not sure what machine can possibly completely test a problem with a 32-bit input space in any "practical" or "reasonable" time.

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.

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.

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.

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

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?

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

Reply on news.ycombinator.com