Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ethereum is Doomed

nakamotoinstitute.org

Post reply on HN
Print view View original

111–120 of 217 posts

Re: Ethereum is Doomed

#111

Post by wyager »

dkarapetyan wrote: post #60
aakilfernandes wrote: post #26

Earlier quoted context omitted.

The whole point of Ethereum is turing completeness. Ethereum without Turing completeness already exists and its called Bitcoin. While this implementation of The Dao has failed, Ethereum is the only blockchain where implementing The Dao is possible.

This doesn't sound right to me. Contract law should not require turing completeness. First order logic should be more than sufficient. How does having a loop in contract law make any sense?

There are also a class of total languages (Coq, Agda, Idris) that are guaranteed to terminate but admit (polymorphic) recursion. This is stronger than FOL but weaker than turing-completeness, and certainly sufficient to implement any feasible contract.

Re: Ethereum is Doomed

#113

Post by dkarapetyan »

wyager wrote: post #109
dkarapetyan wrote: post #19

I didn't know the language was turing complete. Isn't this computing 101? If you want a secure thing then you must be able to reason about it statically. Making things turing complete means any non-trivial property of program correctness can not have a generic solution and so you've just opened yourself up to a world of hurt.

You can reason statically about turing-complete languages. They just have to be syntactically restricted to forms amenable to mathematical analysis. Ethereum's scripting language is poorly designed for this. Many high-tech fintech digital contracts are written in languages like Haskell or Ocaml. Fintech people value strong types, declarative programs, immutability, etc.

Correct. That is what I mean but you still don't just want a restricted subset. You want something that guarantees termination and also lets you reason about any weird runtime behavior and resource usage in a very rigorous way. Some of these things are still research problems and some of them are barely becoming practical in languages like Rust.

Re: Ethereum is Doomed

#114

Post by yarrel »

DennisP wrote: post #22

I have actually tested this attack technique (using my own contracts on a local test chain), and I've been in discussions with some Solidity developers and the guy who first published the attack. The situation is not as bad as this article claims. For starters, you can use address.send(x) instead of address.call.value(x)(). All computations on Ethereum have to be funded with "gas" (transaction fees), and send() only…

Send at the end is like return-once or tail recursion.

Does -

http://www.joeykrug.com/home/a-serpent-send-exploit

change things at all?

Re: Ethereum is Doomed

#115

Post by dkarapetyan »

wyager wrote: post #111
dkarapetyan wrote: post #60

Earlier quoted context omitted.

This doesn't sound right to me. Contract law should not require turing completeness. First order logic should be more than sufficient. How does having a loop in contract law make any sense?

There are also a class of total languages (Coq, Agda, Idris) that are guaranteed to terminate but admit (polymorphic) recursion. This is stronger than FOL but weaker than turing-completeness, and certainly sufficient to implement any feasible contract.

I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.

Re: Ethereum is Doomed

#116

Post by wyager »

dkarapetyan wrote: post #115
wyager wrote: post #111

Earlier quoted context omitted.

There are also a class of total languages (Coq, Agda, Idris) that are guaranteed to terminate but admit (polymorphic) recursion. This is stronger than FOL but weaker than turing-completeness, and certainly sufficient to implement any feasible contract.

I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.

> in a way that is accessible to an average programmer.

The average programmer should not be writing multi-million-dollar contracts.

Re: Ethereum is Doomed

#117

Post by wyager »

dkarapetyan wrote: post #113
wyager wrote: post #109

Earlier quoted context omitted.

You can reason statically about turing-complete languages. They just have to be syntactically restricted to forms amenable to mathematical analysis. Ethereum's scripting language is poorly designed for this. Many high-tech fintech digital contracts are written in languages like Haskell or Ocaml. Fintech people value strong types, declarative programs, immutability, etc.

Correct. That is what I mean but you still don't just want a restricted subset. You want something that guarantees termination and also lets you reason about any weird runtime behavior and resource usage in a very rigorous way. Some of these things are still research problems and some of them are barely becoming practical in languages like Rust.

> You want something that guarantees termination

You usually get that through a restricted subset of an otherwise turing-complete language. The standard approach is to impose a finite metric on the arguments of a function and demonstrate that, as the function recurses, that metric monotonically approaches zero.

>barely becoming practical in languages like Rust.

As far as I know, this cannot be done in Rust. Agda, Coq, and Idris are the primary languages supporting termination checking (because they are syntactically suited for it). Haskell supports it as well through Liquid Haskell.

Re: Ethereum is Doomed

#118

Post by dkarapetyan »

wyager wrote: post #116
dkarapetyan wrote: post #115

Earlier quoted context omitted.

I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.

> in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.

I don't think accessibility is a bad thing. I think computing, its practice and theory, should be taught the same way we teach literacy. I didn't mean "average" as in "incompetent". If writing contracts was as simple as writing a few lines of code in some formal language that didn't require a law or finance degree then I would consider that to be a good thing. It would be even better if the system was designed from first principles with solid theory backing it.

Re: Ethereum is Doomed

#119

Post by wyager »

dkarapetyan wrote: post #118
wyager wrote: post #116

Earlier quoted context omitted.

> in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.

I don't think accessibility is a bad thing. I think computing, its practice and theory, should be taught the same way we teach literacy. I didn't mean "average" as in "incompetent". If writing contracts was as simple as writing a few lines of code in some formal language that didn't require a law or finance degree then I would consider that to be a good thing. It would be even better if the system was designed from f…

I totally agree, but the reality is that in order to write contracts that are sure to be correct, you need a level of expertise that involves much more work than just learning how to write programs. Knowing the syntax and usage of a rigorously-typed language like Agda is the easy part.

Re: Ethereum is Doomed

#120

Post by dkarapetyan »

wyager wrote: post #117
dkarapetyan wrote: post #113

Earlier quoted context omitted.

Correct. That is what I mean but you still don't just want a restricted subset. You want something that guarantees termination and also lets you reason about any weird runtime behavior and resource usage in a very rigorous way. Some of these things are still research problems and some of them are barely becoming practical in languages like Rust.

> You want something that guarantees termination You usually get that through a restricted subset of an otherwise turing-complete language. The standard approach is to impose a finite metric on the arguments of a function and demonstrate that, as the function recurses, that metric monotonically approaches zero. >barely becoming practical in languages like Rust. As far as I know, this cannot be done in Rust. Agda, Coq…

I meant reasoning about resource usage. Rust provides lifetimes which I think is based on linear logic (see https://news.ycombinator.com/item?id=7061876). In theory, this gas thing should act as the metric you mentioned but it doesn't seem like it is implemented properly when it comes to how the fundamental building blocks of Solidity act with respect to the gas metric. The termination stuff in total languages I think has a ways to go in terms of general accessibility. Dependent types aren't the easiest thing to pick up.
Post reply on HN