3 ms·

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

by api 9y ago

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

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

by 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