[Recommendation] Is code the law? Not yet!

Rage Review : The author of this article, Lukas Abegg, is a lawyer with master's degrees in Switzerland and the United States. He discussed the current status and development trend of smart contracts in the context of mathematics, pointing out that it is a challenge for smart contracts to achieve "code is law" at present, so we should not rush into it. Instead, we should gradually solve many existing problems and defects in the process of continuous scientific development and in combination with actual conditions. Moreover, this ancient process can gradually improve smart contracts and increase the enthusiasm of enterprises to adopt this technology.

Translation: Annie_Xu

After the failure of The DAO, people began to heatedly discuss how the Ethereum blockchain should develop and what policies should be formulated.

These include whether to continue to follow immutability and take "code is law" as the most important rule; and what measures to take by consulting Ethereum miners and developers.

Yet little is said about what smart contracts can do.

But I believe this question should be at the heart of the debate, and its answer is the only reasonable basis for formulating the development direction of blockchain and smart contracts.

So let’s take a closer look at the functionality of smart contracts.

The nature of information

The essential characteristic of smart contracts is information processing.

Although there are many definitions of information and no universal definition exists, it is helpful to first explore the way information theory deals with information, because we say that information theory is the DNA of modern computer science.

Therefore, it is necessary to divide information into syntactic information and semantic information. The former is the rules of the relationship between symbols, and the latter is the meaning given to such symbols. However, the boundary between them is usually vague and difficult to distinguish; but the difference between them does exist.

Vitalik Buterin recently wrote an article discussing this difficulty.

Vitalik Buterin

Syntactic information can be analyzed and measured, and can be mathematically proven (as in Shannon and Weaver's "A Mathematical Theory of Communication"). Semantic information is what humans give to symbols; it can represent anything the human mind can think of.

Making semantic information normal and processable is hard. Computer science (especially AI researchers) has had a lot of trouble capturing semantic information and representing it in software, such as natural language. To make matters worse, semantic information can be in very simple or very complex forms.

For example, simple and formal semantic information has patents, which can already be processed in computer languages, such as 3D printing according to the CAD file of a patented gadget.

More complex semantic information, such as the legal definition of "loyalty", cannot currently be processed by computer science, so a great deal of improvement in artificial intelligence research is needed.

Lack of management

Another way to distinguish between the two types of information is to label them "dry code" and "wet code," a term first coined by coder Nick Szabo.

To understand why we respect both sides of information, let’s talk about The DAO. The DAO only has a “do no harm” policy (semantic information) on its homepage, but it is not reflected in the code (the code basically only processes syntactic information).

Believers in the strict doctrine of “code is law” argue that The DAO attackers may be able to keep the ether because the “do no harm” rule is only on the website homepage and not in the code, so it is not binding. Therefore, they continue to support the Ethereum blockchain without forking, creating two parallel Ethereum ecosystems, which brings considerable problems to users and developers.

This fragmentation might not have happened if there were proper management tools to process this semantic information—for example, ensuring that everyone follows the “do no harm” rule and developing ways to deal with violators.

Mathematical proof and immutability

When Shannon began to study communication theory, he was very careful to limit his research to syntactic information, so that he could successfully prove his findings mathematically.

If he had studied semantic information, he would not have succeeded. For Shannon, to advance science, he had to attach importance to mathematical proof methods.

One might think that writing smart contracts doesn’t really advance science, so mathematical proofs are not important. However, once blockchain is added to the code, immutability is achieved; raising the bar for code correctness to incredibly high, if not completely unattainable levels.

Since the code cannot be tampered with, it is necessary to ensure that the code has no loopholes.

So mathematical proofs of code suddenly become a very important feature.

However, Solidity, which is used to implement smart contracts on Ethereum, is not a language that supports mathematical proof methods, but it can implement semantic information, or to be more specific, express the developer's intentions. Just like the developer's design, the "recursive call" used by The DAO hacker originally had a specific purpose.

Apparently the code failed to capture this intent and therefore failed to prevent The DAO funds from being stolen by hackers.

In general, immutability and code correctness are like two ends of a scale. The more you emphasize immutability, the more you need to pay attention to code correctness.

The need for verifiable code

If nearly the entire smart contract runs immutably on the blockchain, it would be nearly impossible to add sufficient “weight” in terms of code accuracy.

These findings are not new.

Back in 200, Nick Szabo wrote a document on formal contract languages ​​in which he made it clear that procedural computer languages ​​might be attractive, but the disadvantages outweigh the advantages. The document did not even mention all the existing programming languages ​​used in the financial industry, or new ways to write programming languages ​​that could provide formal proofs.

Nick Szabo

Even Solidity's developer Dr. Gavin Wood predicted early on that the language would allow developers to perform mathematical proofs; the latest research proves that Solidity must be converted to F* to make the code verifiable.

However, it is now clear that the need for legitimacy, that is, the need for no external parties to the smart contract, has not yet been met and may take a long time to achieve, or may not be achieved at all.

Filling the gap in technology

However, this does not mean that the concept of smart contracts has failed or is meaningless. It just means that we need to face up to the restrictive architecture of existing technology. And there is currently no effective way to bypass the shortcomings of programming languages ​​and artificial intelligence.

This approach may exist in the legal system of the traditional material world, especially in a specific area called "ADR" (Alternative Dispute Resolution).

Its purpose is to provide two or more disputing parties with a formal way to resolve disputes privately, without resorting to the state's public courts. It provides tools that allow you to establish your own rules, define the conflict management process, and select adjudicators.

It also has the nice side effect of implementing constraints in the real world. This is an area worth exploring, such as the futarchy concept of prediction markets, and the new value property of Backfeed for selecting arbitrators. It is not even difficult to put these arbitration rules in smart contracts.

Just make sure that every user of the smart contract service is willing to accept this arbitration rule, just like the arbitration rules that must be followed when registering a domain name (such as ICANN's UDRP).

Achieving Legitimacy

It may seem strange to first study a new field using old concepts.

However, if you look closely at its supporting structure, just like the bracket of a 3D printed object, even if you take it away, the object can still stand on its own, and you will find that there is nothing strange about it. This exploration method is even a bit inspiring, because it can help us understand new concepts and management tools, and perhaps in the future they can completely replace the legal tools in the real world.

Going back to what we said at the beginning, we should respect the dual nature of information, use code to process syntactic information, and use management tools to let humans process semantic information.

While smart contracts are neither smart nor contracts, but simply verifiably verified code, combined with management tools such as smart contract-specific arbitration rules and cognitive technologies, it may be possible to test new technologies in a less disruptive way than what happened with The DAO; and this may be a way to increase the certainty of smart contracts and attract corporate use.

At least until science develops to the stage where “code is law”, a truly legal state can be achieved.