Smart Contracts and Their Issues
Note: This article was first published in Rethinking Law, issue 1, on 31 October 2018.
Since the advent of Ethereum, one of the keystones of blockchain [1] infrastructure has been smart contracts [2]. Technically, as far as we are concerned, a smart contract is nothing more than a piece of code that runs on a blockchain. Having code running on a blockchain means two things: Firstly, being the history of operations happening on a blockchain immutable, smart contracts can be programmed to be immutable as well, in the sense that once they are issued they cannot be revoked. Secondly, all the code on the chain runs in a decentralized fashion: No one but the whole community “holds” the (virtual) machine on which such code is executed.
These two properties make smart contracts particularly appealing for use in law. Immutability means that a smart contract behaves like its traditional counterpart: The only way to make it “disappear” would be by taking down the whole blockchain on which the contract is hosted, which is infeasible. Following a comparison with traditional law, if a contract is signed and protected by a notary then one would have to bribe or get rid of the notary to take it back. The difference is that here the notary is the whole, worldwide community, making this kind of corruption virtually impossible.
Decentralization means that the contract cannot be manipulated. If smart contracts were to run in a centralized fashion, that is, on a centrally managed number of machines, one could change their behavior by seizing the “control room” administering the machines on which they run. Again, in the case of blockchains such a control room doesn’t exist and the machine is distributed worldwide, so this cannot happen. In this respect, smart contracts are even safer than traditional ones, where one has to trust that the notary responsible of safeguarding them won’t misbehave. Clearly the validity of such assumption becomes increasingly disputable as the economic value of the assets ruled by the contract rises.
Not everything is so nice, though. As we said earlier, smart contracts are pieces of code, and as such require a fair amount of technical skill to be properly written. But coders are not lawyers and lawyers are not coders, and in fact law and programming are traditionally considered rather disjoint worlds. This means that the skill set required to write a smart contract properly is incredibly rare to have, requiring competence both from the law side — one must understand what the contract is supposed to do and mean — and from the programming side — one needs to know how to express this properly using code.
To make things worse, the programming languages used to write smart contracts are still highly experimental and incredibly cumbersome to use, even for experienced coders. The natural consequence of this, without diving into technical details, is that it is rather easy to write a smart contract that does not behave as the writer intended. This is somewhat analogous to writing a traditional contract in a sloppy way, creating all sorts of loopholes.
For this reason, great effort is being put by researchers into the blockchain tech all over the world to find better programming languages for smart contracts, that is, better ways to write a contract’s underlying code. To understand how this effort is being directed, it is useful to compare programming and natural languages: There are essentially two reasons why people make mistakes — that is, they convey meaning differently from what they intended — while speaking a language. The first depends on the language itself, as in the case of a word meaning two completely different things that may be wrongly interpreted in some contexts. For instance, “We saw her duck” is one such sentence. The second depends on the language being itself cumbersome and difficult to use. For example, consider a non-native speaker having great difficulty using the grammatical rules of a language correctly.
In the case of programming languages for smart contracts, the majority of research and development efforts are being put into solving problems akin to our first example: The goal is obtaining languages that are semantically unambiguous, and whose behavior is always predictable and deterministic. Loosely speaking, we are trying to get rid of words with double meanings or sentences that can be read in multiple ways.
The Statebox Approach
In this respect, what we do at Statebox is different: We are designing a programming language that also solves problems of the second class. We are not just trying to make the language unambiguous and semantically precise, but also structured in a way that leverages human intuition, meaning that using and learning it should be an easy process. This language has a variety of applications, smart contracts being one of them.
To understand how this is done it is worth mentioning two key features in the Statebox approach and paradigm.
- The first is that our language is completely grounded in mathematics. All the implementation is built upon mathematical concepts and theories that are formally interlinked with each other, the most important ones being category theory, Petri nets and type theory. In particular, category theory is a sort of “mathematics superglue”, that is able to highlight and model links between different mathematical theories in a consistent, formal and well defined way.
- The second is that all the concepts we adopt have a graphical counterpart, called graphical calculus. This is made possible by the fact that some constructions in category theory are proven to be equivalent to a calculus of diagrams, that is, there are theorems [3] that prove how there is no difference between working with these constructions using formulas or drawings: What can be proven is the same. An example of this is given in Figure 1, where an equation and its graphical counterpart are represented. Such results can take us pretty far: Probably one of the most spectacular examples of this is given by categorical quantum mechanics, initially developed by Abramsky and Coecke [4][5], which allows us to express and prove many important results in quantum mechanics diagrammatically: In fact, in Figure 1 you can see part of a quantum process both modeled traditionally and diagrammatically. Albeit they look radically different, they are proven to be equal.
This twofold paradigm has important consequences for people using the language. The first is that the complexity and the mathematics are “hidden” in the images: As long as one knows how the images can be manipulated, knowing the mathematics is not needed. The second is that due to the equivalence between graphical calculi and their mathematical counterparts, one can be sure that what is expressed using images is formally precise and meaningful. In addition to this, Statebox heavily employs type theory to make things even more reliable. Type theory can be thought of as “the watchdog of mathematics” that runs under the hood, unbeknownst to the user. It ensures that the images are manipulated following the right rules, and will prevent the user from making any inadmissible manipulation.
Another benefit of having a programming language grounded in category theory is functoriality: As we have previously stated, category theory is the superglue of mathematics, and it provides tools to map mathematical theories to other mathematical theories. This property can be cleverly used to make Statebox platform agnostic: The Statebox programming language can be applied to any context — or to put it more technically, it can be compiled to any language and architecture — meaning that it can also be used outside blockchain applications. Among the most useful applications of this is the possibility of running Statebox directly on hardware via other tools from theoretical computer science such as logic programming [6], resulting in unmatched speed, efficiency and reliability.
Statebox: Diagrammatic Programming
Let us now dive into how a Statebox program is drafted. In Figure 2 we can see a Petri net. It is composed of places, depicted as blue circles, which hold tokens, depicted as black dots. A place represents a type of resource, while a token in a place stands for a resource of that type. Finally transitions, depicted as gray squares, represent transformations that can turn resources of some type into resources of some other type, as prescribed by the inbound and outbound arcs connecting them to places.
A net represents “the geometry of our code”, and the state of a program is inferred by looking at the distribution of tokens in a net. For instance, consider the net in Figure 3: If the net aims to represent the managing of orders, then we readily infer that there are two open orders, one processed, and three closed. On the contrary, in Figure 4 a single token is used to represent the state of a system, which alternates between two possible “active” and “inactive” configurations.
The great advantage of programming with Petri nets is that one can use them to model how code should work in terms of how the flow of information within it should behave. As shown above, this can be done completely graphically. Using already developed tools [7] it is then possible to check if a state can be reached from another one, that is, if starting from an initial distribution of tokens it is possible to apply transitions and end up having tokens arranged in a target final distribution. Such a property is very useful and allows us to check whether the information flow that we modeled leads to unintended behavior. For instance, one can verify that starting from the net in Figure 5 a distribution of tokens as in Figure 6 cannot be reached.
Only after the net is drafted and the properties we are interested in are verified, it becomes possible to attribute meaning to transitions in the form of bits of code that perform the desired operations. At this point the whole net is compiled — that is, turned into a piece of “traditional” code which can be deployed on some existing platform.
It has to be pointed out how Statebox as a language has way more features than the ones outlined above, such as ways to glue nets together and tools to perform data analytics. The interested reader can take a look at the Statebox monograph, which details the mathematical specification of our language so far [8].
Application in Law
The possibilities of the Statebox programming language are profound when it comes to law. It provides a reliable paradigm to define smart contracts in a way that is compatible with our intuition. It does so while naturally offering a toolkit that enables us to verify whether what we write has the correct properties. Moreover, it requires close to zero coding skills since everything can be done graphically, while turning this into meaningful machine code is taken care of by the link with category theory highlighted in the previous sections.
This is particularly meaningful, since requiring lawyers to become programmers is an unrealistic requirement, if not the biggest obstacle that prevented smart contracts to become a widespread tool in law up to now.
The intrinsic simplicity of Statebox and its low learning curve make it appealing also in terms of the relationship that a law professional can have with clients: With Statebox, a law professional can listen to clients, and, while determining the nature of the contract to be drafted, start expressing it as a net. The client will quickly understand how such nets work, allowing for direct interaction with the professional: Clients can finally understand what is happening and provide direct feedback while the drafting process is still ongoing.
Statebox can also be used to build software infrastructure at any level. Having such infrastructure living on the blockchain is important when transparency and fairness matter, as we would expect with anything regarding the administration of a sovereign state. It is then reasonable to assume that a migration towards a “blockchained state infrastructure” will at some point happen, and that the level of complexity of software hosted on the blockchain — along with its scalability — will grow exponentially in the next years. Reducing such complexity — or to better say making it manageable and understandable — is one of the points where Statebox shines.
When it comes to specific applications of this to law, you can think about the whole computer infrastructure that aids, say, a judge to make a decision in court. This can range from ways to display and store evidence to machine-learning based algorithms that help the judge in making decisions. Much of this infrastructure is, at the moment, proprietary, closed source and not transparent enough, raising often ethical concerns, see e.g. [9]. The right way to implement such tools should instead be as follows: Every time such software is used, a verifiable proof of the computation that happened and led to the result should be produced, including all those hidden parameters that are fed to the software heuristics. In this way it should be possible to verify, at least in principle, if, when and how and a given piece of software misbehaved. To make the process transparent, such proof must be produced and stored on the chain, and even better, one should be able to rerun the computation on different parameters and see the different results, potentially arguing against something that was concluded based on the original parameters used. Moreover, in matters where privacy is concerned, such proofs should also be zero-knowledge, meaning that an hypothetical verifier should be able to check if the proof is correct without knowing or gaining any information about the particular data on which such computation has been run.
We do possess, at the moment, all the needed mathematical infrastructure to turn what we said above into a reality. Nevertheless, the amount of complexity introduced when trying to turn such maths into a reliable implementation is enormous, which is why programming languages as Statebox will be ultimately needed if we want to fix the opaque, non-transparent software infrastructure used now.
Conclusion
Statebox is an ongoing project and we are far from having reached a definitive version of our product. At the moment a minimal viable product consisting of a Statebox language core, a graphical editor for nets and a first implementation of our typesystem are being developed. Nevertheless, it goes without saying that the only true measure when it comes to the effectiveness of a programming language is its adoption, and in this respect we hope to have given enough material to convince the reader of the usefulness of diagrammatic, categorical programming languages for smart contracts, and of their possible uses in law.
[1] Nakamoto, S. (2008). Bitcoin: A Peer-to-Peer Electronic Cash System. www.bitcoin.org, 1–9.
[2] Buterin, V. (2014). A Next-generation Smart Contract and Decentralized Application Platform. Ethereum, 1–36.
[3] Selinger, P. (2010). A Survey of Graphical Languages for Monoidal Categories. In B. Coecke (Ed.), New Structures for Physics (Vol. 813, pp. 289355). Berlin, Heidelberg: Springer.
[4] Abramsky, S., & Coecke, B. (2004). A Categorical Semantics of Quantum Protocols. In Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on (pp. 415–425). IEEE.
[5] Coecke, B., & Kissinger, A. (2017). Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge: Cambridge University Press.
[6] Di Franco, A. (2017). Information-gain Computation. ArXiv:1707.01550 [Cs, Math].
[7] Sobociński, P., & Stephens, O. (2013). Penrose: Putting Compositionality to Work for Petri Net Reachability. In: Heckel, R., & Milius, S. (Eds.), Algebra and Coalgebra in Computer Science. CALCO 2013. Lecture Notes in Computer Science, vol 8089. Berlin, Heidelberg: Springer.
[8] Genovese, F. (2018). The Mathematical Specification of the Statebox Language. Statebox.
[9] Angwin, J., Larson, J., Mattu S., & Kirchner, L. (2016). Machine Bias: There’s software used across the country to predict future criminals. And it’s biased against blacks. ProPublica.
