Hacker News Reader

Hacker News

Comment by api | Hacker News Reader

Parent Full thread

api

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

View on HN

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

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

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.

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

Reply on news.ycombinator.com