[mbenjaminsmith]

I think that's entirely too apologetic. The innovation was the original protocol. They were premature (as a lot of people warned) setting up anything as massive as the DAO, someone found a way to creatively interpret the rules and make a lot of money. Instead of sucking it up as a very expensive bug bounty, they decided to manipulate the entire system -- going against the very essence of that system.

The DAO's own terms state: "Any and all explanatory terms or descriptions are merely offered for educational purposes and do not supercede or modify the express terms of The DAO’s code set forth on the blockchain; to the extent you believe there to be any conflict or discrepancy between the descriptions offered here and the functionality of The DAO’s code at 0xbb9bc244d798123fde783fcc1c72d3bb8c189413, The DAO’s code controls and sets forth all terms of The DAO Creation."

Obviously the hacker's intent was theft but under the DAO's own terms it was a valid activity.

Basically the code is law. If we're going to then interpret that law then we've created a system similar to the current systems we have, but lacking in maturity. The point of something like Ethereum is not that it can't be manipulated, it's that it doesn't need to be in order to function. It can be trusted explicitly because its functionality is not open to interpretation.

If I'm not being clear enough -- what they should have done is taken this as a very expensive lesson and otherwise left the system alone. Yes, a "bad person" would have profited but the system's integrity would have been untouched.

FWIW, I was an early backer of Ethereum and bought ETH during the pre-sale. I invested because I thought it was promising -- without any real expectation of return. Coincidentally I sold all of my ETH just before this hack (40x ROI). Because of the fork I would not invest in ETH again, regardless of potential returns, because Ethereum is no longer what it set out to be.

[AstralStorm]

Why would anyone want code that is not mathematically proven to become law?

Yes, even with modern automatic theorem provers it is a bit torturous. But people are even going so far as writing a mathematically proven safe kernel (1) and Ethereum is much smaller and simpler.

(1) https://sel4.systems/

[larkery]

I think you raise a good question; I further wonder whether the provability of outcomes is even sufficient to justify the kind of total procedural adherence which the ethereum folks (until recently!) advocated.

In normal contract law that doesn't have a blockchain in it there is a special moral "backstop" where a judge may find a contract to be unconscionable. An unconscionable contract may contain nothing forbidden by statute, but if it is found to be profoundly unjust in terms of its outcomes (not due to change in circumstance, but as a result of its formulation), then a judge can call the contract unconscionable and it is void.

This kind of latitude is really valuable, as it recognises the fact that things are pretty complicated and that in the end the law is there to ensure justice, not to mechanically interpret a set of rules.

So, even if you have a smart contract (or as I would call it "program") which can be proven to work a certain way, that may not be enough to guarantee that it is not going to give rise to bad outcomes. For example, say we have a proof showing that the program obeys some invariants, and one may even have such a proof generated automatically. This makes us feel confident - let us irreversibly bind our future actions to the output of the program! Blockchains be praised!

However, if the real invariant being aimed for is that the program's execution is "justice-preserving" (and I would say this is a good aim), then there is a grounding problem we have missed, where the prover needs to specify formally the nature of a just situation or action.

I believe a large number of person-years have already been spent on attempts to derive such an "ethics predicate", but if anyone has found it they have not yet bothered to demonstrate it. As a result if we wish to pursue justice, we end up falling back to the position taken by the ordinary law, and we might wonder quite why we decided to use 51% of all computing power for the rest of time to keep a ledger intact in the first place.

[chopin]

Proven against what? The intentions of coder? In that case the intentions need to be codified. With that, we are back to square one I think.

[drdeca]

If a contract is sufficiently simple, it seems to me like it could make sense.

However, I do think it is, or perhaps, would have been, important to put a lot of focus on moving to mathematically proven contracts.

[tomp]

> The DAO's own terms state: "..."

Would the "hacker" have a chance to win in court? The DAO/Ethereum administrators are obviously breaking the terms of the contract...

[CoryG89]

I have read somewhere previously that someone claiming to be the hacker came forward anonymously and said they would indeed take it to court if they lost the funds due to intervention via a fork[1]. Who knows if this was really the hacker, or whether it was a credible threat even assuming it was.

[1]: http://pastebin.com/CcGUBgDG

[ifdefdebug]

I don't think so, because if he claims "the code" is everything and even if the judges accept that argument, then the logical consequence is that, if "the code" allows for a hard fork, then the hard fork is "the code" as much as his attempt to drain funds.