Hacker News Reader

Comment by aakilfernandes | Hacker News Reader

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.

View on HN

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?

Would regular payments based on criteria be an example? A paycheck basically.

This argues for a temporal logic, not for recursion. Something like: http://szabo.best.vwh.net/contractlanguage.html

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.

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.

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.

Then the platform is flawed. Average programmers should be able to understand it easily.

It's not that hard, some wants X and some wants Y in exchange.

I'm not a lawyer but I write contracts with my clients. If you keep things simple it should fit most people. making g smart contracts complicated you keep it in the area of a small elite who are knowledgeable of playing safe with it.

I wold go as far as make it as simple as HTML.

That's what standardized contracts are for. Tellers don't write the legalese on your credit card receipt. They just print it out.

But : https://en.wikipedia.org/wiki/Solidity "As specified by Wood it is designed around the ECMAScript syntax to make it familiar for existing web developers;"

I agree. Furthermore, the notion of contracts that cannot be specified in first-order logic seems relatively dangerous to me.

Could you expand on how one would specify DAO-like contracts with only first-order logic?

There is a huge canyon between "you can use this small set of ops" and "turing complete".

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.

> Ethereum without Turing completeness already exists and its called Bitcoin.

There are an infinite number of non-Turing complete languages. Not-Turing complete != Bitcoin.

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.)

>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 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.

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!

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.

> 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.

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.

Reply on news.ycombinator.com