There will probably be a hardfork and increased moral hazard for auditing contract code. Why spend money finding bugs if the "immutable" blockchain can be rolled back?
Well, "traditional" law can be changed as well, so I'm not sure why a blockchain should not be able to. Some changes are more controversial than others, but in the end the majority (more or less) decides. Either by vote in congress/senate, or by users picking a particular client/chain.
Ethereum has had one particularly controversial fork, and so did Bitcoin. In both cases, both chains survived, with one significantly more popular than the other (in both hash rate, transactions, and market cap). (Un)fortunately, traditional law in real life does not permit two realities to coexist, so there the analogy falls apart somewhat.
Well, national currencies do get "forked"[1], but this would be like if they did extremely narrow forks to fix problems of someone's own stupidity, and only the stupidity of the most important people.
Like, imagine if twenty members of congress kept their life savings in cash in uninsured briefcases and surprise, those briefcases were stolen. And they responded by passing emergency legislation invalidating the specific serial numbers stolen, and requiring every merchant and bank to screen for those serial numbers (and not those from any other e.g. bank robbery).
I would consider that kind of action to be very delegitimizing to the currency.
[1] I would consider it to be analogous to a fork when they e.g. deprecate an old design or migrate to the Euro.
Well blockchains work by consensus is the difference: the rules can only be changed if enough people agree. This sounds better in principle but breaks down using proof of work when a small number of parties control most of the computing power.
Once again, this is supposed to be better than, and different from, "traditional" law! It has no purpose if the contracts don't actually do what they say. The whole point is that computers evaluate the contracts and do what they say.
As seanwilson says above, blockchains work by consensus. Leaving aside the "better", that does mean it is different. The instructions are still executed by computers as it was programmed as you say, but if enough users/miners agree this was not the intention of the contract/code, they can fork.
I do think that calling blockchains "immutable" can be confusing to users not familiar with the concept and its nuances. And I personally hold no opinion on whether the currently locked up funds need to be returned to their owner with a fork. There is something to be said for both options, specifically in this case where there the "rightful owner" is clear (like the other cases mentioned in https://github.com/ethereum/EIPs/issues/156 ).
I don’t know if probably is the right word. There might be a hard fork there might not. The DAO hack was only three months after the Homestead release. You could credibly say Ethereum was in beta. I think over a year later that’s no longer true.
At the time of the DAO hack there also hadn’t been a public demonstration of the scale and danger of contract hacking. That’s also no longer true.
That said, ETH is an anarchist federation in the end, and the market will decide which reality is most valuable: the one in which the parity hack happened or the one in which it didn’t.
Pact (http://github.com/kadena-io/pact) is a turing-incomplete LISP (no recursion, no lambdas, no unbounded loops ... no macros either ;) ) and built in Haskell. Also has formal verification by directly compiling to SMT-LIB2 (not released yet, but watch a demo! https://youtu.be/l7XuSuEe-Yg?t=22m23s).
Does this move the bugs from the implementation language to the language of the verification spec? Or is there a way to express some generic requirements such as "don't strand assets"?
Presumably one would have to first formalize that constraint (taking care, for example, that 'not stranded' is not being satisfied by someone stealing the assets), and then, unless the language makes it impossible, prove that it is not violated anywhere. In Solidity, it is a long deductive chain from the specific bug here to the realization that it could lead to stranding.
Https://cardanohub.org looks promising. Haskell, peer reviewed, formally verified. They're working on the compute layer though, so no smart contracts yet but Philip Wadler (one of the godfathers of haskell) is working on that. It's is promising because they actually hire programming language academics to work on the technology
“Code is Law” fails again.
There will probably be a hardfork and increased moral hazard for auditing contract code. Why spend money finding bugs if the "immutable" blockchain can be rolled back?