6 ms·

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

by VMG 9y ago

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?

api 9y ago
"Code is law" demands much better code. A language like Haskell is needed.
- chowells 9y ago
  Eh. Haskell is a general purpose Turing-complete language. Smart contracts need something far safer.
  - arianvanp 9y ago
    How about http://statebox.org http://statebox.org?
  - sciyoshi 9y ago
    There's also Simplicity, which is not Turing complete and includes formal verification with Coq https://news.ycombinator.com/item?id=15588380 https://news.ycombinator.com/item?id=15588380
  - spopejoy 9y ago
    Pact (http://github.com/kadena-io/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://youtu.be/l7XuSuEe-Yg?t=22m23s).
- arianvanp 9y ago
  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
- VMG 9y ago
  A Bitcoin developer is working on a formally verifiable language: https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017-October/015217.html https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017...
  - digikata 9y ago
    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"?
    - mannykannot 9y ago
      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.
  - scottlocklin 9y ago
    I'm not sure formal verification would have helped here. A linter would have helped.
- CryptoPunk 9y ago
  Bamboo is a formally verifiable programming language being developed for Ethereum: https://github.com/pirapira/bamboo https://github.com/pirapira/bamboo The Bamboo manifest: https://github.com/pirapira/bamboo/blob/master/doc/manifest.md 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 https://runtimeverification.com/blog/?p=411
tyrust 9y ago
The proposed fix is not a rollback.
- VMG 9y ago
  "Changing the consensus rules to revert the state to a more desirable one for this instance" is more correct
  - deleted 9y ago
    [deleted]
erikpukinskis 9y ago
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.
pietjepuk88 9y ago
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.
- SilasX 9y ago
  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.
- draw_down 9y ago
  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.
  - pietjepuk88 9y ago
    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 https://github.com/ethereum/EIPs/issues/156 ).
xiphias 9y ago
It can only be rolled back if Vitalik has money in that contract... otherwise it's immutable
mlvljr 9y ago
Wow, is the comment dead or the author? As I think I saw both "alive" yesterday.

by VMG 9y ago

api 9y ago

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

chowells 9y ago
Eh. Haskell is a general purpose Turing-complete language. Smart contracts need something far safer.
- arianvanp 9y ago
  How about http://statebox.org http://statebox.org?
- sciyoshi 9y ago
  There's also Simplicity, which is not Turing complete and includes formal verification with Coq https://news.ycombinator.com/item?id=15588380 https://news.ycombinator.com/item?id=15588380
- spopejoy 9y ago
  Pact (http://github.com/kadena-io/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://youtu.be/l7XuSuEe-Yg?t=22m23s).
arianvanp 9y ago
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
VMG 9y ago
A Bitcoin developer is working on a formally verifiable language: https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017-October/015217.html https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2017...
- digikata 9y ago
  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"?
  - mannykannot 9y ago
    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.
- scottlocklin 9y ago
  I'm not sure formal verification would have helped here. A linter would have helped.
CryptoPunk 9y ago
Bamboo is a formally verifiable programming language being developed for Ethereum: https://github.com/pirapira/bamboo https://github.com/pirapira/bamboo The Bamboo manifest: https://github.com/pirapira/bamboo/blob/master/doc/manifest.md 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 https://runtimeverification.com/blog/?p=411

tyrust 9y ago

The proposed fix is not a rollback.

VMG 9y ago
"Changing the consensus rules to revert the state to a more desirable one for this instance" is more correct
- deleted 9y ago
  [deleted]

erikpukinskis 9y ago

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.

pietjepuk88 9y ago

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.

SilasX 9y ago
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.
draw_down 9y ago
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.
- pietjepuk88 9y ago
  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 https://github.com/ethereum/EIPs/issues/156 ).

xiphias 9y ago

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

mlvljr 9y ago

Wow, is the comment dead or the author? As I think I saw both "alive" yesterday.