4 ms·

One of the cool things about Ethereum is that you can build your non-turing-complete contract software on Eth, and use Eth to check your NTC-Eth contracts. I c

One of the cool things about Ethereum is that you can build your non-turing-complete contract software on Eth, and use Eth to check your NTC-Eth contracts. I can't think of anything stopping you from doing this right now. Maybe you or other people can weigh in on why it's not feasible?

SomeStupidPoint 10y ago
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!

SomeStupidPoint 10y ago

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!