After The DAO experiment failed, a heated policy debate ensued about how to go forward with the development of ethereum’s blockchain.
The positions ranged from holding on to the immutability paradigm with “code is law” as the most important rule to follow, to a more human approach of asking ethereum’s miners and developers what measures should be taken.
Only little time, however, was spent on the question what a smart contract is actually capable of performing.
But this very question, I believe, should be at the core of the debate and the respective answer is the only sensible foundation on which a sound policy for blockchain and smart contract development can be built.
So let’s take a closer look at the capabilities of smart contracts.
Nature of information
The feature of a smart contract is in its very essence the processing of information.
While the notion of information varies and no universal definition exists, it is helpful to start with the way information theory deals with information since information theory is part of the DNA of today’s computer science.
It is therefore necessary to divide information into syntactic information and semantic information. The former being the rules about the relationship between symbols and the latter being the meaning attributed to such symbols (ie: “intent”). The line between the two is somewhat blurry and telling them apart is sometimes difficult (which, as we see later, lead to the DAOs problem in the first place) but a difference between them clearly exists.
An interesting piece about the difficulty of capturing “intent” was recently written by Vitalik Buterin.
Syntactic information can be parsed and measured (as Shannon and Weaver did in “A Mathematical Theory of Communication”) and is open to mathematical proof. Semantic information, however, is what a human being attributes to a symbol. It may represent anything a human brain is capable of thinking about.
Normalising semantic information and making it processable is quite a difficult task, to put it mildly. Computer science (in particular artificial intelligence researchers) struggles a great deal in trying to capture semantic information, such as natural language, and represent its meaning in software. To make matters worse, semantic information can be anything from quite simple to very complex.
Rather simple and formal semantic information, like a patent for example, can already be processed by computer language. Think a CAD file of a patented widget on a computer that lets a 3D printer print out the exact thing that said CAD file contains.
More complex semantic information, like the legal notion of “good faith” for instance, cannot yet be handled by computer science. To do so, a great leap in artificial intelligence research is still needed.
Missing governance
Another way of making a distinction between these two types of information would be referring to them as “dry code” and “wet code”, a concept coined by cryptographer Nick Szabo.
To make a point about why it is imperative to respect that two-sided nature of information, we may look at The DAO. The imperative of “doing no harm” (ie: semantic information) was only written on The DAO’s home page and not in its code (which, for the most part, processed syntactic information only).
Followers of a strict “code is law” doctrine argued that The DAO hacker might therefore keep the drained ether since the “do no harm” imperative was only in the home page’s specifications but not in the code itself and therefore not binding. They took their case even further by holding on to the non-forked ethereum blockchain and created a parallel ethereum environment, ethereum classic, which produces some quite tricky problems for users and developers.
If there had been a proper governing tool that would have dealt with semantic information (ie: ensured everybody abides to the “do no harm” rule and provided means to deal with violators), such split would probably not have happened.
Mathematical proof and immutability
When Shannon worked on the theory of communication, he took great care that his research was confined within the syntactic information realm. That allowed him to mathematically prove his findings.
That could not have been done if semantic information was involved. For Shannon, mathematical proof was important in order to advance science.
Coding a smart contract does not really advance science and therefore mathematical proof is not important, one might think. However, as soon as you add immutability through a blockchain implementation to your code, you are raising the bar for the correctness of your code to an incredibly high level, if not completely out of reach (cf: more detailed analysis).
Since your code is immutable and cannot be changed, you need to be perfectly sure your code has no flaws.
Mathematical proof of your code, therefore, seems all of a sudden quite an important feature to have.
And yet, Solidity as used on ethereum for smart contract implementation, is not a language that allows for mathematical proof (ie: is not referentially transparent). It allowed for the implementation of semantic information, or put explicitly, the developers’ intent. The recursion-call that led to The DAO hack should have been used in a specific way, as the developers intended it.
Obviously, such intent was not captured by the code and therefore didn’t hinder The DAO hacker from draining The DAO.
In conclusion: immutability and correctness of code are like the two pans of a scale. The more “weight” you put on immutability the more care you have to take regarding the correctness of your code.
Need for verifiable code
If almost your entire smart contract is immutably running on the blockchain (like some “code is law” enthusiasts envision it to be the only way to go) you are most likely not able to put enough “counter weight” into the correctness of your code.
All of these findings are far from being news.
Already back in 2002, Nick Szabo wrote a paper about a formal language for contracts, in which he explicitly pointed out that the use of procedural computer language may be tempting but causing more harm than good. This doesn’t even mention all the existing programming languages that are used in the financial industry or new ways of creating program languages, which allow for formal proving (samples here and here).
Even the developer of Solidity itself, Dr Gavin Wood, envisioned in an early stage of Solidity’s conception a language that allows for mathematical proof and the newest research is suggesting that the translation of Solidity into F* to reach verifiable code would be needed.
However, it seems clear by now, that the desired state of alegality, where no engagement from outside a smart contract is needed, is not reached yet. And it will probably still take quite some time to get there, if it can be reached at all.
Filling the technical void
That does not mean, however, that the concept of smart contracts has failed or would be useless. It just needs an architecture that respects the limits of current technology. And a clever work-around for the gaps in programming language and artificial intelligence that yet need to be filled.
Such a work-around might lay in the legal system from the classic meatspace, in particular a specific area called Alternative Dispute Resolution (ADR).
Its purpose is to give two or more arguing parties the formal means to resolve their disputes in private without having to resort to public state-run courts. It provides tools that allow you to set up your very own rules, define the processes of how to manage conflicts, and/or select the judges of your choice.
It has also the nice side effect of being actually classic-meatspace-legally binding. It is a formidable playing field to explore, eg: futarchy ideas like prediction markets or new value attribution concepts like Backfeed for choosing an arbiter. And it’s not even very difficult to implement such arbitration rules into a smart contract.
Just make sure every user of a smart contract service accepts to be subjected to such arbitration rules, just like you are subjected to privately constituted arbitration rules (eg: the ICANN’s UDRP) when registering a domain name.
How such a link between smart contracts and meatspace-legal rules might look like can be found here. (These are not ADR rules but contract law rules. The implementation, however, would be very similar).
Moving towards alegality
At first, it might look odd to use old concepts in order to advance into a new area.
However, if you look at it as support structures – very much like a freshly 3D printed item has and which can steadily be moved away when the new item stands in its own capacity – the oddness fades. Even more, such a way to move forward might even have a heuristic element in the sense that it helps to learn more about new concepts and tools of governance that might replace meatspace-legal tools completely in the future.
To come full circle with the beginning, we should respect the two-sided nature of information and let code process syntactic information and deploy governance tools for human beings to process semantic information.
Using a governing tool like smart contract specific arbitration rules in combination with the recognition that smart contracts are neither smart nor contracts but rather just verifiably executed code (VEC) may provide a way to test new technology in a less disastrous way than it was done with The DAO and may also provide the certainty needed to make smart contracts interesting for businesses.
At least until science catches up with the vision of “code is law” and a true state of alegality can be reached.
Golf image via Shutterstock