7 ms·

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

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.

aakilfernandes 10y ago
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.
- TylerE 10y ago
  There is a huge canyon between "you can use this small set of ops" and "turing complete".
  - jacques_chester 10y ago
    Not really. Any language that has sequential instructions, branching and loops is Turing complete, per the Structured Programming Theorem. Given how hard it is to avoid accidentally introducing these three "simple" elements, Turing completeness often turns up without being planned for.
- drdeca 10y ago
  There is a thing that advertises itself as being like Ethereum but without the Turing completeness. It is meant to be able to do more computation based stuff than Bitcoin, but without being Turing complete. However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.)
  - wtallis 10y ago
    >However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.) They seem to be related concepts. See http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 for discussion of some interesting examples: > [...] has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses. Adam has also constructed a 4,888-state Turing machine that halts iff there’s a counterexample to Goldbach’s Conjecture, and a 5,372-state machine that halts iff there’s a counterexample to the Riemann Hypothesis.
    - drdeca 10y ago
      I didn't mean that the two aren't related, just that they aren't as strongly related as the group seemed to be implying. They were saying that Ethereum being turing complete made it inconsistent in some way. But yes, the two definitely are connected. For example: A program which could solve the halting problem would be able to determine whether a given system is consistent. So, as a result, if a system could prove that a program solved the halting problem, and it could simulate programs running, then it could simulate the program that solves the halting problem being applied to a program that searches for inconsistencies in the system. This would allow it to prove whether it is itself consistent. Therefore, by Godel's second incompleteness theorem, a system which can simulate programs for any number of steps, and which is consistent, and which can do arithmetic and such, cannot prove that any particular program solves the halting problem. Admittedly, this is a lot weaker than "no program solves the halting problem", but I think it is a fairly clear connection. So, yes, I agree that they are related. But Ethereum's Turing completeness (or, Turing completeness except being limited by gas costs), does not mean that Ethereum is "inconsistent", because that is, uh, pretty much a nonsense claim. And that is the claim that I think the other group was making (Though they may have stopped making it since.) Also, btw, wrt that blogpost, they got the number of states for a machine which ZFC cannot prove does not halt, but which does not halt, down to, iirc, like 2030 ? But you probably knew that already because it is the next blogpost on there. But yeah that is a cool result!
- dkarapetyan 10y ago
  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?
  - conception 10y ago
    Would regular payments based on criteria be an example? A paycheck basically.
    - naasking 10y ago
      This argues for a temporal logic, not for recursion. Something like: http://szabo.best.vwh.net/contractlanguage.html http://szabo.best.vwh.net/contractlanguage.html
  - wyager 10y ago
    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.
    - dkarapetyan 10y ago
      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.
      - wyager 10y ago
        > in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.
        dkarapetyan 10y ago
- intrasight 10y ago
  I also don't see the relevance of it being TC. I've heard regex is TC. Wouldn't want to write a contract in regex.
  - wyager 10y ago
    > I've heard regex is TC. You heard wrong. Regex is specifically not turing complete. It corresponds to the class of machines called DFAs. Above regexes are CFGs, which correspond to pushdown automata. Above CFGs are CSGs, which correspond to linear bounded automata. Above CSGs are unrestricted grammars, which correspond to turing machines. You may be thinking of PCREs, which aren't actually regular expressions, but are sometimes erroneously referred to as such. I don't know if those are turing complete or not.
  - SolarNet 10y ago
    By definition regular expressions are not Turing complete... There is an ordering relationship between turing machines and regular expressions which explicitly states regular expressions are strictly a subset of turning machines. This is automata theory 101. Ask for a refund from your school. Jesus what has this field come to.
- naasking 10y ago
  > Ethereum without Turing completeness already exists and its called Bitcoin. There are an infinite number of non-Turing complete languages. Not-Turing complete != Bitcoin.
eternalban 10y ago
Another VC funded outfit I chatted with also boast of TC. This is, I agree with you, software engineering 101. But that's probably it: don't know about you, but I could not stomach making a pitch for funding for the latest hype [1] knowing that the fundamentals are unsound. I am hoping that the recent events -- Theranos, out-smarted contracts, etc. -- will permit a return to maturity in this field. Money has poisoned this field. [1]: wrote about (genetically) evolving cellular corporation back in '96 so this is not a case of I don't get it.
rtpg 10y ago
Well for one it costs you money to run the programs so if you want to run your program forever you can try that but it's a bit of a money pit. I think the idea vehind TC is that now you could write in certain styles that do guarantee termination without sacrificing readability. For example if you're working with just primitively recursive functions you can always guarantee termination So the prerequisite for people investing is for the contract to be in a certain style, or something EDIT: besides, even without TC you still need to check the contract for logic bugs. TC is a bit of a red herring for "due diligence is always needed"
plaguuuuuu 10y ago
Turing completeness isn't so bad when you have a relatively low gas limit on a transaction that ensures you can halt at some point. Maybe I spent too much time in functional languages and I've been doing too much React stuff lately but the way I see it, we have Contract_method(state, parameters) => {new state, return value} You could always run the program on a fake, mock state then test postconditions for sanity. So, if those postconditions pass and we haven't run out of gas, run the program for real, otherwise return an error. Eg transferring 30 eth from contractA to contractB you would have one of the postconditions asserting that ContractA balance is the old balance minus 30. The notion of gas implies a stack or effort limit, so it's guaranteed that any operation will eventually fail once it runs out of resources. Thus you can specify a theoretical upper limit on resources used in pre-verification, which (AFAIK)is paid by the client contract that requests to withdraw money from the other contract. I guess one could avoid this by using a DSL that is formally verifiable, but it's still an interesting option
- dkarapetyan 10y ago
  Yes, I'd assumed since Ethereum was so highly touted and hyped that the foundations of the entire thing were sane. Well I mean sane in the sense that the actual contract language was as restrictive as possible and custom made for expressing contract law but it turns out you can do arbitrary computation and although in theory you're limited by this gas thing because the language is not formally specified and verified it is not clear at all if there are no other bugs lurking around with respect to bypassing the gas bounds. What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece.
  - naasking 10y ago
    > What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece. Actually, termination checkers often compare the size of the term being reduced before and after an evaluation step, and if it can prove that it's always smaller, then termination is assured. With the notion of finite amounts of gas, termination seems assured, so this termination analysis can (and should) be added to EVM. Based on this termination property, all sorts of static analyses now become possible.
wyager 10y ago
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.
- dkarapetyan 10y ago
  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.
  - wyager 10y ago
    > 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.
    - dkarapetyan 10y ago
      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 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.
deleted 10y ago
[deleted]

aakilfernandes 10y ago

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.

TylerE 10y ago
There is a huge canyon between "you can use this small set of ops" and "turing complete".
- jacques_chester 10y ago
  Not really. Any language that has sequential instructions, branching and loops is Turing complete, per the Structured Programming Theorem. Given how hard it is to avoid accidentally introducing these three "simple" elements, Turing completeness often turns up without being planned for.
drdeca 10y ago
There is a thing that advertises itself as being like Ethereum but without the Turing completeness. It is meant to be able to do more computation based stuff than Bitcoin, but without being Turing complete. However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.)
- wtallis 10y ago
  >However, they seem to have confused the halting problem not being computable with Godel's second incompleteness theorem? (They might have corrected this since I saw when they published something with this.) They seem to be related concepts. See http://www.scottaaronson.com/blog/?p=2725 http://www.scottaaronson.com/blog/?p=2725 for discussion of some interesting examples: > [...] has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses. Adam has also constructed a 4,888-state Turing machine that halts iff there’s a counterexample to Goldbach’s Conjecture, and a 5,372-state machine that halts iff there’s a counterexample to the Riemann Hypothesis.
  - drdeca 10y ago
    I didn't mean that the two aren't related, just that they aren't as strongly related as the group seemed to be implying. They were saying that Ethereum being turing complete made it inconsistent in some way. But yes, the two definitely are connected. For example: A program which could solve the halting problem would be able to determine whether a given system is consistent. So, as a result, if a system could prove that a program solved the halting problem, and it could simulate programs running, then it could simulate the program that solves the halting problem being applied to a program that searches for inconsistencies in the system. This would allow it to prove whether it is itself consistent. Therefore, by Godel's second incompleteness theorem, a system which can simulate programs for any number of steps, and which is consistent, and which can do arithmetic and such, cannot prove that any particular program solves the halting problem. Admittedly, this is a lot weaker than "no program solves the halting problem", but I think it is a fairly clear connection. So, yes, I agree that they are related. But Ethereum's Turing completeness (or, Turing completeness except being limited by gas costs), does not mean that Ethereum is "inconsistent", because that is, uh, pretty much a nonsense claim. And that is the claim that I think the other group was making (Though they may have stopped making it since.) Also, btw, wrt that blogpost, they got the number of states for a machine which ZFC cannot prove does not halt, but which does not halt, down to, iirc, like 2030 ? But you probably knew that already because it is the next blogpost on there. But yeah that is a cool result!
dkarapetyan 10y ago
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?
- conception 10y ago
  Would regular payments based on criteria be an example? A paycheck basically.
  - naasking 10y ago
    This argues for a temporal logic, not for recursion. Something like: http://szabo.best.vwh.net/contractlanguage.html http://szabo.best.vwh.net/contractlanguage.html
- wyager 10y ago
  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.
  - dkarapetyan 10y ago
    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.
    - wyager 10y ago
      > in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.
      - dkarapetyan 10y ago
intrasight 10y ago
I also don't see the relevance of it being TC. I've heard regex is TC. Wouldn't want to write a contract in regex.
- wyager 10y ago
  > I've heard regex is TC. You heard wrong. Regex is specifically not turing complete. It corresponds to the class of machines called DFAs. Above regexes are CFGs, which correspond to pushdown automata. Above CFGs are CSGs, which correspond to linear bounded automata. Above CSGs are unrestricted grammars, which correspond to turing machines. You may be thinking of PCREs, which aren't actually regular expressions, but are sometimes erroneously referred to as such. I don't know if those are turing complete or not.
- SolarNet 10y ago
  By definition regular expressions are not Turing complete... There is an ordering relationship between turing machines and regular expressions which explicitly states regular expressions are strictly a subset of turning machines. This is automata theory 101. Ask for a refund from your school. Jesus what has this field come to.
naasking 10y ago
> Ethereum without Turing completeness already exists and its called Bitcoin. There are an infinite number of non-Turing complete languages. Not-Turing complete != Bitcoin.

eternalban 10y ago

Another VC funded outfit I chatted with also boast of TC. This is, I agree with you, software engineering 101. But that's probably it: don't know about you, but I could not stomach making a pitch for funding for the latest hype [1] knowing that the fundamentals are unsound. I am hoping that the recent events -- Theranos, out-smarted contracts, etc. -- will permit a return to maturity in this field. Money has poisoned this field. [1]: wrote about (genetically) evolving cellular corporation back in '96 so this is not a case of I don't get it.

rtpg 10y ago

Well for one it costs you money to run the programs so if you want to run your program forever you can try that but it's a bit of a money pit. I think the idea vehind TC is that now you could write in certain styles that do guarantee termination without sacrificing readability. For example if you're working with just primitively recursive functions you can always guarantee termination So the prerequisite for people investing is for the contract to be in a certain style, or something EDIT: besides, even without TC you still need to check the contract for logic bugs. TC is a bit of a red herring for "due diligence is always needed"

plaguuuuuu 10y ago

Turing completeness isn't so bad when you have a relatively low gas limit on a transaction that ensures you can halt at some point. Maybe I spent too much time in functional languages and I've been doing too much React stuff lately but the way I see it, we have Contract_method(state, parameters) => {new state, return value} You could always run the program on a fake, mock state then test postconditions for sanity. So, if those postconditions pass and we haven't run out of gas, run the program for real, otherwise return an error. Eg transferring 30 eth from contractA to contractB you would have one of the postconditions asserting that ContractA balance is the old balance minus 30. The notion of gas implies a stack or effort limit, so it's guaranteed that any operation will eventually fail once it runs out of resources. Thus you can specify a theoretical upper limit on resources used in pre-verification, which (AFAIK)is paid by the client contract that requests to withdraw money from the other contract. I guess one could avoid this by using a DSL that is formally verifiable, but it's still an interesting option

dkarapetyan 10y ago
Yes, I'd assumed since Ethereum was so highly touted and hyped that the foundations of the entire thing were sane. Well I mean sane in the sense that the actual contract language was as restrictive as possible and custom made for expressing contract law but it turns out you can do arbitrary computation and although in theory you're limited by this gas thing because the language is not formally specified and verified it is not clear at all if there are no other bugs lurking around with respect to bypassing the gas bounds. What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece.
- naasking 10y ago
  > What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece. Actually, termination checkers often compare the size of the term being reduced before and after an evaluation step, and if it can prove that it's always smaller, then termination is assured. With the notion of finite amounts of gas, termination seems assured, so this termination analysis can (and should) be added to EVM. Based on this termination property, all sorts of static analyses now become possible.

wyager 10y ago

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.

dkarapetyan 10y ago
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.
- wyager 10y ago
  > 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.
  - dkarapetyan 10y ago
    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 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.

deleted 10y ago

[deleted]