Hacker News Reader

Comment by dkarapetyan | Hacker News Reader

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.

View on HN

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.

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

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.

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

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.

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.

Ah, that's an interesting idea. Static resource usage analysis instead of computation tokens.

> Dependent types aren't the easiest thing to pick up.

Look at liquid types. They're a lot easier to leverage in practice. Liquid Haskell is all just comments on top of a regular Haskell program.

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.

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.

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!

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?

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.

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

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

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"

Reply on news.ycombinator.com