[jude-]

> While others have pointed out that this is wrong, it's worth amplifying: Turing machines are deterministic. You can run the contract locally and observe how it behaves, and it will behave the same way in the same environment elsewhere. If this wasn't the case, you couldn't have consensus at all.

"Deterministic" != "feasible to reason about halting states for all inputs." Running it locally to see how it behaves for a handful of inputs is definitely not sufficient for claiming that the code behaves correctly (i.e. is "secure").

Recall that people lost money in the DAO not because they didn't test how the DAO behaved when they sent their Ether to it. They lost money because someone discovered the contract as implemented did not behave the way it was expected and advertised to behave. Had it been possible to reason about the DAO's halting states for all possible inputs, the re-entrance bug would have been caught and fixed before the DAO was released.

[nmca]

Formal analysis will help sort this out. Larry Paulson trained up these guys: https://www.imandra.ai/

And similar tech can be applied to smart contracts. Would have spotted the DAO bug. Not ready for prime time yet, but will be around the same time as sharding maybe...

[jude-]

That's much easier said than done. If formal methods were practical, we'd be using them already everywhere else.