4 ms·

I'm personally waiting on an ETH successor with non-Turing-complete, verifiable code. There's no reason that smart contracts require Turing completeness (no re

I'm personally waiting on an ETH successor with non-Turing-complete, verifiable code. There's no reason that smart contracts require Turing completeness (no real world program requires it, for that matter), and software theorem proving will be required for me to take smart contracts seriously. We need to be able to prove things about the contract execution for it to be safe to trust "code as contract". Im not as upset about the hardfork as many people, though. Social constructs should be changable by politics, not indelible and absolute. That's not what they were selling, but all the same, what they were selling was dystopian nonsense where humans are chained to machines, not their masters. It's a feature not bug of social constructs to be changeable through politics. What matters is the political process to do so.

merlincorey 10y ago
I think this is a great response, especially because I agree with the first part, and the second part gave me more to think about. > I'm personally waiting on an ETH successor with non-Turing-complete, verifiable code. Absolutely! My premise is that with turing completeness comes more chances for shooting in the foot. > Im not as upset about the hardfork as many people, though. Social constructs should be changable by politics, not indelible and absolute. That's not what they were selling, but all the same, what they were selling was dystopian nonsense where humans are chained to machines, not their masters. It's a feature not bug of social constructs to be changeable through politics. What matters is the political process to do so. This is great insight. I think for me, personally, the problem I have is that it seems like there isn't much politics involved at all... a completely centralized and small group made a decision and the great majority of users followed right along (as we would expect them to). This is not quite how it is (or was anyway) sold to people as a concept.
- computerwizard 10y ago
  Checkout Byteball. I think it has a strong future and the technology is novel. https://Byteball.org https://Byteball.org
  - chm 10y ago
    They advertise a "fair" distribution. Note that 98% of all bytes and blackbytes will be distributed to current Bitcoin holders who bother to prove their Bitcoin balances during at least one of distribution rounds. and that Then the number of bytes and blackbytes you receive in each round will be proportional to the balance of your Bitcoin address in the snapshot block of that round. So the rich get richer, again. This is not "fair" in the sense that I thought they meant ;)
natosaichek 10y ago
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.
hdhzy 10y ago
Why not just use Bitcoin? [0] [1] [0]: https://en.bitcoin.it/wiki/Contract https://en.bitcoin.it/wiki/Contract [1]: https://curiosity-driven.org/bitcoin-contracts https://curiosity-driven.org/bitcoin-contracts
thepain 10y ago
> We need to be able to prove things about the contract execution for it to be safe to trust This is a very valid concern, in my opinion. Although some people seem to be working on that, it looks like still in its infancy: https://medium.com/@pirapira/1-000-ether-bounty-on-a-proven-correct-wallet-with-17-instructions-just-a-beginning-41edadc96321#.jxhlsayup https://medium.com/@pirapira/1-000-ether-bounty-on-a-proven-... I'm also afraid that 'smart contract' is sort of a misnomer. Where regular "social" contracts between people and entities define all sorts of relationships, the contracts that are put on a blockchain-serialized VM can only express relationships in terms of value transfers.

merlincorey 10y ago

I think this is a great response, especially because I agree with the first part, and the second part gave me more to think about. > I'm personally waiting on an ETH successor with non-Turing-complete, verifiable code. Absolutely! My premise is that with turing completeness comes more chances for shooting in the foot. > Im not as upset about the hardfork as many people, though. Social constructs should be changable by politics, not indelible and absolute. That's not what they were selling, but all the same, what they were selling was dystopian nonsense where humans are chained to machines, not their masters. It's a feature not bug of social constructs to be changeable through politics. What matters is the political process to do so. This is great insight. I think for me, personally, the problem I have is that it seems like there isn't much politics involved at all... a completely centralized and small group made a decision and the great majority of users followed right along (as we would expect them to). This is not quite how it is (or was anyway) sold to people as a concept.

computerwizard 10y ago
Checkout Byteball. I think it has a strong future and the technology is novel. https://Byteball.org https://Byteball.org
- chm 10y ago
  They advertise a "fair" distribution. Note that 98% of all bytes and blackbytes will be distributed to current Bitcoin holders who bother to prove their Bitcoin balances during at least one of distribution rounds. and that Then the number of bytes and blackbytes you receive in each round will be proportional to the balance of your Bitcoin address in the snapshot block of that round. So the rich get richer, again. This is not "fair" in the sense that I thought they meant ;)

natosaichek 10y ago

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.

hdhzy 10y ago

Why not just use Bitcoin? [0] [1] [0]: https://en.bitcoin.it/wiki/Contract https://en.bitcoin.it/wiki/Contract [1]: https://curiosity-driven.org/bitcoin-contracts https://curiosity-driven.org/bitcoin-contracts

thepain 10y ago

> We need to be able to prove things about the contract execution for it to be safe to trust This is a very valid concern, in my opinion. Although some people seem to be working on that, it looks like still in its infancy: https://medium.com/@pirapira/1-000-ether-bounty-on-a-proven-correct-wallet-with-17-instructions-just-a-beginning-41edadc96321#.jxhlsayup https://medium.com/@pirapira/1-000-ether-bounty-on-a-proven-... I'm also afraid that 'smart contract' is sort of a misnomer. Where regular "social" contracts between people and entities define all sorts of relationships, the contracts that are put on a blockchain-serialized VM can only express relationships in terms of value transfers.