3 ms·

The ETH language semantics aren't what I'd want for verification proofs, even restricted to a subset. It's possible there are conflicts between the execution mo

The ETH language semantics aren't what I'd want for verification proofs, even restricted to a subset. It's possible there are conflicts between the execution model and what would be required for verified, secure contracts. Similarly, Id want a proof-checked VM for the currency, which ETH is pretty far from supporting. So verified-ETH would be a larger, more bug-prone project than starting from first principles, developing a language and VM in parallel. (Also, starting a new project gives a chance to change the economics and/or technology used; depending on your views, this might be a benefit.)

Tezos 10y ago
https://tezos.com/pdf/language.txt https://tezos.com/pdf/language.txt
Jabanga 10y ago
Yoichi Hirai has built a formal definition of the EVM in Coq which makes it possible to produce formal proofs of an Ethereum smart contract's correctness: https://medium.com/@pirapira/ethereum-virtual-machine-for-coq-v0-0-2-d2568e068b18#.gndxjlug7 https://medium.com/@pirapira/ethereum-virtual-machine-for-co...
- SomeStupidPoint 10y ago
  Thanks for showing me this! I either missed it or it didn't exist last time I looked in to ETH. (About a year ago, pre-DAO.) Either way, this is a major component of what I'd like to see in smart contracts! (The other two major pieces being a verified VM that supports that spec, and a developer library of "standard" contract pieces -- I don't recall being impressed by directly coding for the EVM, and easy-to-use contracts require a library of "standard legalese".) Glad to see ETH is putting in the effort.
  - Jabanga 10y ago
    Most welcome! It was just released so you wouldn't have seen it last year. There was a major push toward more secure smart contacts, in particular using formal verification, after the DAO hack, and the efforts continue to this day.
    - pirapira 10y ago
      Using my definition of EVM, I think it's already possible to create a small verified compiler. My priority is on keeping the formal definition in sync with the Yellow Paper and the implementations.
      - Jabanga 10y ago
        It's a surprise to see you here! :) Thanks for the explanation. Good luck with your work!

Tezos 10y ago

https://tezos.com/pdf/language.txt https://tezos.com/pdf/language.txt

Jabanga 10y ago

Yoichi Hirai has built a formal definition of the EVM in Coq which makes it possible to produce formal proofs of an Ethereum smart contract's correctness: https://medium.com/@pirapira/ethereum-virtual-machine-for-coq-v0-0-2-d2568e068b18#.gndxjlug7 https://medium.com/@pirapira/ethereum-virtual-machine-for-co...

SomeStupidPoint 10y ago
Thanks for showing me this! I either missed it or it didn't exist last time I looked in to ETH. (About a year ago, pre-DAO.) Either way, this is a major component of what I'd like to see in smart contracts! (The other two major pieces being a verified VM that supports that spec, and a developer library of "standard" contract pieces -- I don't recall being impressed by directly coding for the EVM, and easy-to-use contracts require a library of "standard legalese".) Glad to see ETH is putting in the effort.
- Jabanga 10y ago
  Most welcome! It was just released so you wouldn't have seen it last year. There was a major push toward more secure smart contacts, in particular using formal verification, after the DAO hack, and the efforts continue to this day.
  - pirapira 10y ago
    Using my definition of EVM, I think it's already possible to create a small verified compiler. My priority is on keeping the formal definition in sync with the Yellow Paper and the implementations.
    - Jabanga 10y ago
      It's a surprise to see you here! :) Thanks for the explanation. Good luck with your work!