Hacker News Reader

Comment by srtjstjsj | Hacker News Reader

Ethereum/DAO would be much less of a tire fire embarassment if the management had taken some time to learn anything about the basics of contracts and law, instead of making it up as they go and assuming the entirety of centuries of civilization has no clue what they were doing.

View on HN

    assuming the entirety of centuries of civilization has no
    clue what they were doing

This is a common assumption in these circles, unfortunately.

I think that there is an interesting outlook here. It seems to me that some people are under the impression that the world is essentially simple, and it is stupid people and institution that complicate it. If we apply careful mathematical reasoning, we could find better solutions to anything.

The interesting thing is that about 100 years ago some mathematicians believed something similar about math itself. They believed that since we have formal procedures to reason about math, eventually we'd be able to understand (i.e. prove) everything we want to know. That hope was finally crushed by the discovery of simple, finite, small mathematical objects, that while subject to mathematical reasoning, are able to forever elude complete understanding and proof. Those objects inhabit a very large, unbridgeable gap between our ability to reason and our ability to fully understand (and prove). Those objects, of course, are what today we call computer programs.

If there's anything that proves beyond any doubt that even systems that operate according to a small set of rules, and subject to mathematical reasoning and manipulation, are still able to defy complete understanding -- even in theory, let alone in practice -- it is computer science.

Yet, even though computer science is the very discipline that proved that complexity that can arise even in the smallest of systems is essential and cannot ever be tamed, it is computer scientists and software developers who often attempt to challenge the very foundation of their own discipline.

Yes! I read a great comment here (I forgot by whom) that said something like

    It's hard enough to prove that a computer program will
    actually *do* something, forget about proving what the
    program *will not* do.

He was arguing against the idea that Turing complete languages should be used in smart contracts. The person mentioned that it's not trivial to even assign a complexity category to the question asked, let alone getting an answer (if you can).

Right, although "Turing complete" is a red herring here, as we can't generally verify the behaviors of programs written in most non-Turing complete languages either. I wrote in another comment that if we place computational power on a scale and put Turing completeness at 10 and FSM at 1 (0 being no computation at all, i.e, return the input), then the computational power that we can always generally verify would lie somewhere between 0 and 1. Even FSMs are PSPACE-complete to verify, meaning we can only generally verify small ones (which is why software verification isn't about finding a language in which all programs are tractably verifiable -- as it is unlikely that such a language would be very useful -- but rather to try and verify specific programs that form a small subset of all possible program, regardless of the computational model of the language they're written in).

So the general intractability of computation is essential and far from limited to Turing completeness. If you find this subject interesting, I'll be giving a talk about it next month[1] (it will be recorded).

[1]: http://curry-on.org/2016/sessions/why-writing-correct-softwa...

Cool, I am indeed interested. I read Aaronson's "Quantum Computing Since Democritus" and enjoyed it, but that's the only source I read concerning computational complexity.

They were indeed very naive. In the history of law, there has always been a divide between those who believe that the letter of law should be applied no matter what, and those who believe that social justice should be ensured. Whatever the terms of theDAO, there WILL be judges to find that what just happened to it is theft. That is why instead of damaging trust in Ether by forking it, the ethereum/DAO management should turn to the law to get its money back.

Smart contracts are a very good thing, but they won't become perfectly safe any time soon (if ever), so the community should recognize that civil and criminal law are a safety net, likely to help smart contract get wider use, because of they create increased trust.

> Whatever the terms of theDAO, there WILL be judges to find that what just happened to it is theft.

I am not completely sure if it went to court and it was litigated fully it would be found that the theDAO smart contracts that were buggy could be rolled back to what was "intended" as there was language that specifically denied that form of reasoning. theDAO clearly fucked up but that doesn't invalidate a contract. The intent in the contract was actually clearly declared, the smart contract was binding in its form. The smart contract's intent was its code. It's code was buggy. Thus one will have to litigate in court whether intent can inferred from buggy code and whether a software bug can be rules as outside of intent. Rolling back transactions like that are really exceptional.

I think it is quite interesting. A lot of people in the stock market have lost money because of software bugs, although everyone didn't agree beforehand that that software was the intent. I think it could go either way with theDAO's software contract if it was litigated.

That said you could possibly sue the implementers of the smart contract for negligence to try to recover the loss, or those that advertized theDAO as a viable investment vehicle for false advertizing or misleading one about safety, both of those are much more straight forward legal avenues.

Its not that civilization has no clue what they are doing. It just hasn't integrated technological advances fully.

The recent problems were very technical and specific as well as being solvable from a number of approaches.

Reply on news.ycombinator.com