The title may not make sense, but it's catchy. Here we look at the issue od Decidability and human action - which may be a better title.
# Intent is fundamentally complex.
The philosophy behind this fact has been best formalized by the friendly AI research community, where is bears the names of “complexity of value” and “fragility of value“.
The thesis is simple: we as human beings have very many values, and very complex values – so complex that we ourselves are not capable of fully expressing them, and any attempt to will inevitably contain some uncovered corner case.
The utility of the concept to AI research is important because a super-intelligent AI would in fact search through every corner, including corners that we find so unintuitive that we do not even think of them, to maximize its objective.
Tell a superintelligent AI to cure cancer, and it will get 99.99% of the way there through some moderately complex tweaks in molecular biology, but it will soon realize that it can bump that up to 100% by triggering human extinction through a nuclear war and/or biological pandemic.
Tell it to cure cancer without killing humans, and it will simply force all humans to freeze themselves, reasoning that it’s not technically killing because it could wake the humans up if it wanted to – it just won’t. And so forth.
In smart contract land, the situation is similar. We believe that we value things like “fairness”, but it’s hard to define what fairness even means.
You may want to say things like “it should not be possible for someone to just steal 10000 ETH from a DAO”, but what if, for a given withdrawal transaction, the DAO actually approved of the transfer because the recipient provided a valuable service?
But then, if the transfer was approved, how do we know that the mechanism for deciding this wasn’t fooled through a game-theoretic vulnerability? What is a game-theoretic vulnerability?
What about “splitting”? In the case of a blockchain-based market, what about front-running? If a given contract specifies an “owner” who can collect fees, what if the ability for anyone to become the owner was actually part of the rules, to add to the fun?
All of this is not a strike against experts in formal verification, type theory, weird programming languages and the like; the smart ones already know and appreciate these issues.
However, it does show that there is a fundamental barrier to what can be accomplished, and “fairness” is not something that can be mathematically proven in a theorem – in some cases, the set of fairness claims is so long and complex that you have to wonder if the set of claims itself might have a bug - blog.ethereum.org
# See also * Intuitionistic logic - wikipedia