> The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program halts, period.

Exactly, knowing that the contract code will eventually halt is nice to know but knowing that it will halt after a reasonable CPU cost seems much more important in this case (which is really interesting).

From what I've seen from example contracts, it doesn't seem like the chance of infinite loops is that high. Personally, I find that in mainstream languages, if you accidentally write an infinite loop you find out very quickly on the first few runs and code that could be hiding an infinite loop stands out. The vast majority of loops just iterate from the start of a collection to the end.

The contract coders I work with try as much as possible to avoid loops altogether, because even if they're correct, they'll still have a linear cost, and that's usually not what you want. Almost all contract operations should be O(1). Sometimes we've made fairly large system design changes to avoid a loop in a function.

Interesting. So what's your view about the most practical language for writing contracts in then?

For what I've read, having the sender setting gas limits seems really awkward especially when the limit is exceeded. Are there practical alternatives? Even with O(1) you'd need to limit the computation time.

I don't have a fully formed view yet, but I think Solidity is a pretty good prototyping language, disregarding all marketing hype that it's an "easy" language. While developing, you'd also be working on a specification of exactly how the contract shall behahve, and trying very hard to simplify ruthlessly.

The Parity multisig contract is very complex and I wouldn't and didn't trust any funds with it. I hope that the newly deployed fixed multisigs are bug-free but how would you know?

Right now I'm working on tools for static analysis of bytecode and using such tools to verify the correctness of contracts written by hand in assembly, which I think makes a great deal of sense for the simple contracts that we need as utilities (multisigs, tokens, etc).

> The Parity multisig contract is very complex and I wouldn't and didn't trust any funds with it. I hope that the newly deployed fixed multisigs are bug-free but how would you know?

Yeah...any ideas why they didn't go with a language that had an easier route for formal verification? It seems like an ideal application and the contract specifications seem like they would be fairly straightforward to prove (compared to what you'd see in most journal papers for instance). I'm guessing the designers just weren't aware of theorem provers but I'm puzzled why they didn't go with a language with strong static typing where private access and immutability are the defaults plus avoiding anything to do with the mechanism they have for picking default handling functions when a message isn't understood. Great experiment to watch though!