Indeed. All you have to do is test every possible input, in much the same way that any computation on a real computer is technically decidable because the limited amount of RAM means that it can only have a finite number of states. Neither of those limits actually makes solving the problem feasible in practice.

>Neither of those limits actually makes solving the problem feasible in practice.

That's the point. Theoretical limitations has no bearing on solving the practical problem. That is why RichardHeart's original point [1] is wrong.

[1] The halting problem states you can't predict what a turing complete program will do, until you run it. This means to some degree, that you can't predict what your "smart" contract will do, until it does it. Thus turing completeness causes security to be far, far harder than non turing completeness. This is how you lose the millions of dollars as the DAO did after it passed audits.

Pretty sure the parent was saying the opposite. Testing every possible input is infeasible, since the number of possible inputs (and number of possible states) is HUGE.

That is not the opposite of what I said. That is a reason why what I said is true.

Parent said "Neither of those limits actually makes solving the problem feasible in practice." This is correct, since the input space is too huge to feasibly explore. Yes, it is technically correct that there are a finite number of states that your laptop can be in. No, it does not mean that I can practically enumerate all possible states my code can be in.

Formal verification will be necessary in practice. This is not an ideal outcome either, since (1) you have to formally specify the problem you're trying to solve and (2) the proof that the code meets the specification can easily be bigger than the program, by many orders of magnitude. Even this does not guarantee that bugs won't happen, since there's no guarantee that your specification accurately describes the problem you're solving.

> This comment is simply incorrect. The gas limits do make smart contracts decidable. It is a mathematical fact.

This line of reasoning does not help me write better code, and does not address the parent's concerns. Using this argument, I can say that every single program I will ever run in my lifetime is also decidable, since eventually the computer I'm using to run it will stop working. This of course does not mean that I will write bug-free code, nor does it mean that I will write code that is feasible to prove correct.

What I want is a decidable programming language where it is always feasible to reason about the smart contract's halting states for arbitrary input. Bitcoin and its derivatives let me do this. Ethereum does not.

Sure it does - the marvelous thing about a turing-complete virtual machine is that you can write a decidable language that compiles to EVM bytecode.

Sorry, I didn't qualify "always feasible" well enough. What I meant was, I want it to be feasible to reason about the halting states of every single smart-contract that will ever interact with my code. Not just the ones that I write, but also the ones that are reachable from my smart contract's call graph, and the ones that call into my smart contract.

If I can do this, then I can feasibly reason about how my code will react to other peoples' inputs (e.g. I can prove the absence of DAO-like re-entrance bugs). The fact that Ethereum allows smart contracts to be written in undecidable languages means that this is not feasible in practice.

I don't think I follow - why would you need to reason about your callers' internal states in order to prove properties about your own contract?

Because in practice, I'm trying to reason about the consequences of submitting a given transaction. A transaction can invoke many smart contracts in addition to mine. It's not enough for my code to be correct; every piece of code the transaction causes to run has to be correct as well.

If you want to know what a given transaction will do, you can simply run it locally; no need for formal analysis. Formal analysis is useful for proving properties about your program like "the total balance will always equal the sum of the accounts" and "transfers never increase the sender's balance".

I want to know what any possible transaction can do. See my sibling comments.

But you can reason about what any possible transaction can do by reasoning about all possible inputs to your code; you don't need to know anything about how other contracts were written, since even if they are formally provable, they could send you literally any input.

Edit: Rereading your earlier comment, I understand now - you're talking about other contracts your code calls, not vice-versa. In that case, I'd point out that you're totally free to either write those contracts yourself if they're not already provably secure, or write your own code such that it's formally proved to work regardless of what those contracts do.

> But you can reason about what any possible transaction can do by reasoning about all possible inputs to your code; you don't need to know anything about how other contracts were written, since even if they are formally provable, they could send you literally any input.

I also have to reason about the transactions that invoke other smart contracts that, through one or more subsequent calls, will call into mine. These transactions are inputs to my smart contract as well. Recall that the DAO was hacked by an "attacker" contract that called into it, for example.

> I'd point out that you're totally free to either write those contracts yourself if they're not already provably secure, or write your own code such that it's formally proved to work regardless of what those contracts do.

If formal specification and verification were practical, we'd be doing it in every programming domain. Normally, few people bother since (1) it takes a lot of work, and (2) the consequences of bugs are small in most domains, especially compared to the consequences of not shipping code on time. If you have not tried to formally specify and verify the correctness of a non-trivial program before, I encourage you to try it before recommending that strategy (especially if that recommendation includes telling developers to rewrite other peoples' code).

Since smart contracts have other peoples' money attached to them, the developers' first priority must be user safety. Ethereum does not appear to take this seriously, since (1) its default programming languages are not designed to be amenable to formal verification, and (2) smart contracts are allowed to call into one another.

I would much rather program on a blockchain that kept smart contracts completely isolated from one another, and required me to submit a machine-checked proof that the user's money (1) will be sent to an address of the user's choice automatically no more than X blocks after the deposit, and (2) cannot leave the smart contract at an earlier time without a one-time-use signature from the user. If a smart contract cannot be proven to do both of these things, then the blockchain should prevent it from running.