Earlier this month we released source code for the blockchain language Simplicity.
Simplicity is our answer to the problems faced when trying to code sophisticated smart contracts in blockchain environments. Prior to Simplicity, blockchain programming languages typically made tradeoffs between expressiveness and reliability; developers could either build a complex but unreliable smart contract, or a very basic but reliable one. With Simplicity, developers can finally design sophisticated smart contracts and be confident in their outcomes.
Simplicity has been built to be compatible with Blockstream’s Elements platform. That means developers building sidechains or independent blockchains on Elements will soon be able to take advantage of the features enabled by Simplicity. As an implementation of Elements, the Liquid Network will also support Simplicity; opening up interesting applications for Liquid users, such as trust-minimised escrow, vaults, and other more complex smart contracts.
The source released this month 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.
- A technical report detailing the Simplicity language.
Why Simplicity?
Blockchains pose several unique challenges that make traditional programming languages unsuitable.
- All users must all agree on the result of a computation in all environments.
- Each participant in a smart contract must be aware of all possible results for all possible inputs to a program upfront.
- All users must be able to prevent denial of service attacks that would consume excessive memory or computation time.
- Each participant in a smart contract must be able to understand the costs of their program execution for all possible inputs upfront.
Existing programming languages designed specifically for blockchains, such as Ethereum’s EVM, still face these challenges. Recently, an EVM upgrade failed during testing because implementations did not agree on the result of a computation. Funds have been stolen or otherwise unrecoverable due to smart contract logic errors and programs that exceed their resource limits.
On the other hand, Bitcoin’s Script language is generally limited to combinations of digital signature checks, timelocks, and hashlocks. While impressive protocols (such as the Lightning Network) have been built on these primitives, Bitcoin’s Script language lacks the expressiveness needed for more complex smart contracts.
Simplicity aims to provide the flexibility and expressiveness for whatever computations you need, while allowing you to verify the safety, security and costs of your smart contracts.
What is Simplicity?
Simplicity is a low-level programming language and machine model for blockchain-based smart contracts. It is designed from the ground up to have simple semantics which lend themselves to static analysis and reasoning by formal methods. The Simplicity language is defined by its implementation in the Coq proof assistant.
While the core language itself is simple enough that it fits on a T-shirt – simplicity of a language does not translate to simplicity of development. There are a few reasons for this:
- Blockchains involve a fundamentally different programming model than ordinary programming. The job of a blockchain is to verify computation, rather than to do computation. This is a subtle distinction, but an extremely powerful one because it is possible to verify arbitrary code execution, without the need for Turing-completeness.
- Once deployed, a smart contract is immutable and this leaves no room to correct for mistakes. Simplicity addresses this problem by empowering users to create formal proofs of correctness for their smart contracts.
- Simplicity is extremely low level language for direct execution, more akin to assembler language than to Java or Python. Ultimately we expect users will write their contracts in one or more higher-level languages which would then be compiled to Simplicity.
What’s New?
Since we last blogged about Simplicity, we have been working hard to move from experimental language research to a more formal language specification.
We have reimplemented the Simplicity language in the Coq proof assistant:
- We have denotational semantics of the full Simplicity language, including language extensions that support witness data, assertions, and delegation.
- A formal specification of an abstract machine called “the Bit Machine” based on free categories provides operational semantics for the core Simplicity language.
- A Haskell implementation developed in tagless final style lets you experiment with evaluating, executing, and type-checking Simplicity expressions.
- A modular approach to Simplicity language extensions allows you ignore the effects of language extensions when you are not using them.
- We have a host of Simplicity expressions for cryptographic primitives, including our own reimplementation of libsecp256k1 in Simplicity.
- A technical report that provides an informal mathematical specification of the Simplicity language, and provides guides for the Coq and Haskell developments.
While Simplicity development is still ongoing, we have reached a point where developers can now explore the Simplicity language themselves. Therefore, it is time to move Simplicity development into the open and open a mailing list.
What’s Next
Going forward, there are many fronts for Simplicity development.
For our part, we plan to:
- complete the C interpreter.
- implement a library of jets for various common cryptographic functions.
- use Verifiable C to prove our C interpreter and jets are correct.
- integrate Simplicity into the Elements blockchain platform.
Other fronts of development include:
- Development of Simplicity code optimizers.
- Creating new or adapting existing high-level smart contract platforms, such as Ivy, for generating Simplicity.
- Combine the functional correctness of Simplicity’s cryptographic primitives with formal correctness of cryptographic protocols to build fully verified smart contracts.
We hope you will join us in our project.