When we think of smart contracts, we usually associate them with the two major programming languages: Bitcoin’s Script and Ethereum’s Solidity. Other examples include Cardano’s Marlowe and Plutus, Tezos’ Liquidity, and plenty of other developments that serve different purposes. However, the biggest issue with these languages is that the parties which sign a smart contract must be able to comprehend and analyze all the possible outcomes that may result from the code. Furthermore, a deployed smart contract cannot be modified, so the act of signing one requires intensive deliberation and an absolute agreement between the parties.
This is where Blockstream’s Dr. Russel O’Connor steps in and proposes a blockchain programming language whose functions and semantics fit on a t-shirt. The first presentation of Simplicity has been made on October 30th 2017 in anticipation for PLAS 2017 (Programming Languages and Analysis for Security), and the proposed 34-page paper cites the works of industry heavyweights such as Satoshi Nakamoto, Adam Back, Peter Todd, Vitalik Buterin, Greg Maxwell, and C.P. Schnorr (among many others).
The last time we heard of Simplicity was during Dr. Connor’s presentation from BPASE 2018 back in February. But this fall, Blockstream appears to be the most consistent company to release new products and services: after launching the Liquid federated sidechain and the privacy-oriented block explorer, now they have enriched their ecosystem with the addition of the source code for Simplicity.
According to the latest blog post on the matter, this release includes “Denotational semantics of the core Simplicity language and its extensions formally specified in Coq, operational semantics of the core Simplicity language formally specified in Coq, an interpreter, type-checker, and serialization of the Simplicity language written in Haskell, Example Simplicity expressions, including cryptographic operations such as SHA-256 and EC-Schnorr signature verification, and a technical report detailing the Simplicity language.”
Why would anyone use Simplicity?
The first arguments presented by the Blockstream team involve the issues and limitations of the other programming languages: Ethereum’s EVM has recently had a failed upgrade where the implementations did not agree on the computation results, and there are instances where funds were stolen and became unrecoverable due to security breaches. Conversely, Bitcoin’s script relies on three criteria (digital signature checks, timelocks, and hashlocks) and therefore has limited expressivity.
In order to overcome these shortcomings, Blockstream’s Simplicity offers a simpler syntax and semantics that are more akin to Java and Python, formal proofs of correctness to allow smart contract parties to edit certain provisions that they agree on, and a code compiler which functions without the need of Turing completeness. In other words, programming smart contracts will become a lot easier for coders who are used to basic languages, parties which find loopholes in their smart contracts can mutually come to terms to make modifications, and even more high-level languages can be compiled to Simplicity.
This launch is special because the development has been moved into the open to allow other experts in the field to peer review the code and make suggestions to its improvement. In this regard, a dedicated GitHub for Simplicity has been created and the interested parties can join a mailing list.
Pros and cons of Blockstream’s Simplicity
Clearly, Simplicity is a useful project which brings smart contracts closer to mass adoption. It simplifies the programming language while allowing more expressivity than Bitcoin’s Script, it brings inter-operability with other languages by attempting to be a universal compiler, it allows for smart contracts to be amended in a secure way, and it’s integrated with Blockstream’s Elements platform which also opens up opportunities to develop for the Liquid Network.
The research paper looks impressive and references the works of some of the biggest heavyweights of cryptography and blockchain development, and the fact that the code was released in the open is a sign that the protocol while a mailing list gets built follows the cypherpunk ethos which is paramount in this field.
On the other hand, there are two types of criticism that can arise from this early phase of the project. First of all, it’s going to be interesting to see how the implementation of formal proofs of correctness actually works. Removing the immutability of smart contracts and allowing parties to make edits via consensus is a concept that is more akin to the amendments we make to real-life contracts.
It’s like inserting a dollar bill into the coffee machine thinking that it’s going to cost two dollars, the coffee company wants to double the price due to an unexpected shortage of coffee beans, but it can’t operate the change without your explicit consent. In the past, it was all about time-stamping the moment when the purchasing agreement is made and the first dollar bill gets inserted, so no modifications can be made in the whole process regardless of the long-term fairness of the deal.
In theory, it sounds great. In practice, it can open the gates of hell for plenty of abuses and inconveniences which make smart contracts less appealing to the masses. Immutability, despite having its bugs, is the killer app for blockchains and the true value of the functions that they operate comes from this feature.
The second wave of criticism can come from the regular “Blockstream is centralizing power” argument. It’s a bad idea to rely too much on the services of one company, and in the future we may see Blockstream turn into the Google of blockchains. On the plus side, all of their projects are transparent, privacy-friendly, and built by true experts who understand the legitimate concerns that enthusiasts have. The fact that their contributions are mostly open-source and anyone can review the code is also a factor which strengthen’s Blockstream’s position as a legitimate company, but it’s important to keep the cypherpunk ethos alive and constantly verify instead of building too much trust.
Simplicity is a fine addition which deserves praise, and it’s likely that efforts like Dr. Russel O’Connor’s will bring mass adoption through increased accessibility. After all, it was Xerox that invented the graphic user interface for operating systems, but it wasn’t until Steve Jobs picked it up and implemented it in Apple’s Macintosh that we saw a popularization and adoption of the technology.
Crypto Insider has contacted Dr. Russel O’Conor and asked for a comment on how formal proof of correctness works. His response was the following:
“Developers can use formal methods to prove programs correct and have software proof assistants verify every logical step. Simplicity is going to empower smart contract developers to really prove the correctness of their contracts so that parties can safely and securely transact with each other.”
Cover image credit: Blockstream