Hacker News Reader

Comment by VMG | Hacker News Reader

Reposting dead, but accurate comment:

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

View on HN

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.

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

Well, turns out that it is in fact worse, not better.

Isn't the whole point that this shouldn't be like traditional law and can't change because it's in code?

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.

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.

The proposed fix is not a rollback.

"Changing the consensus rules to revert the state to a more desirable one for this instance" is more correct

It can only be rolled back if Vitalik has money in that contract... otherwise it's immutable

"Code is law" demands much better code. A language like Haskell is needed.

Eh. Haskell is a general purpose Turing-complete language. Smart contracts need something far safer.

How about http://statebox.org?

There's also Simplicity, which is not Turing complete and includes formal verification with Coq https://news.ycombinator.com/item?id=15588380

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

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

A Bitcoin developer is working on a formally verifiable language: https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017...

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.

I'm not sure formal verification would have helped here. A linter would have helped.

Bamboo is a formally verifiable programming language being developed for Ethereum:

https://github.com/pirapira/bamboo

The Bamboo manifest:

https://github.com/pirapira/bamboo/blob/master/doc/manifest....

There is a project under way to formalize Viper, which is the other newly developed programming language for Ethereum, as well:

https://runtimeverification.com/blog/?p=411

Reply on news.ycombinator.com