How to prevent another DAO disaster?

What happened today to the DAO could have happened to any other smart-contract platform... probably except one. TauChain is a programmable blockchain based on ontologies & reasoning and it's an extremely interesting attempt to address the very problem that caused the DAO's melt-down: human inability (or unwillingness) to reliably predict the outcome of code execution.

TauChain aims to offer a virtual machine for smart contracts, similar to EVM (Ethereum Virtual Machine) but with one important advantage: any code will be automatically and deterministically verified before being executed. In other words, the Proof of Code Execution feature will allow TauChain to predict with 100% reliability all possible outcomes of code execution before it is actually run. So no malicious or harmful code can pass the test. And there can be no unexpected outcomes. Pretty amazing, isn't it?

The only downside of TauChain is the fact that it does not support Turing completeness. This stems from the fundamental law of our universe discovered and proved by Kurt Gödel: any language (including a programming language) can either be complete (in our case Turing complete) or consistent (in our case verifiable), but it can never be both.

According to TauChain's creators, Turing incompleteness is not a serious disadvantage, as you don't really need it for writing smart-contracts, even the most complex ones.

My knowledge is not deep enough to be able to judge whether TauChain's approach is indeed the ultimate solution. I've done some initial research on TauChain but still there are many aspects I haven't found answers for.

The major unknown for me is this: TauChain's main assumption seems to be that it is much easier to write a smart-contract's specification (or verification test) than the actual implementation. My experience tells me that creating a test that covers all edge cases is pretty hard as well. So is it indeed practically possible to create a reliable verification test for a complex smart-contract?

Maybe somebody here at Steem can shed some light on this.