The emergence of blockchains and smart contracts has seen a widespread interest in building dapps and leveraging smart contracts for practical purposes. Solidity — a smart-contract language of Ethereum — is the primary programming language used for Ethereum’s public blockchain network and remains the most popular widespread smart contract language.
Despite its success and widespread use for writing smart contracts on Ethereum, Solidity is a relatively new programming language, naturally susceptible to bugs and some high-level logical faults. Out of the demand for smart contract creation and improved security methods for writing them, programming languages Vyper and Scilla have emerged.
Solidity & Smart Contracts
Solidity was proposed by Gavin Wood back in 2014 and is the dominant programming language for writing smart contracts. It is specifically designed for the Ethereum Virtual Machine (EVM) and features some useful documentation on what it is and how to use it.
Solidity is available to learn about on multiple online educational platforms — including Udemy — and has several extensive books written about it. The networks effects of Solidity have cemented it as the go-to programming language for smart contracts and dapps built on Ethereum.
Despite its widespread popularity, Solidity’s existence as an EVM-specific programming language limits its use for other blockchain platforms. Further, security concerns around high-level languages and their potential problems have led to an emphasis on smart contract auditing and simpler as well as more secure languages. High-profile hacks and research studies revealing the sheer size of vulnerabilities inevitably has led to a pressing need for better smart contract practices.
Vyper is an experimental programming language that is similar to Solidity in that it is also tailored specifically to the EVM. Vyper is syntactically similar to Python and is contract-oriented like Solidity.
However, Vyper is designed with the specific goals of security, simplicity, and auditability. This is largely a result of security issues in early smart contract iterations. As a consequence of Vyper’s principals and goals, explicit examples of features that it purposefully does not have are outlined as:
- Class Inheritance
- Function & Operator Overloading
- Recursive Calling
- Infinite Loops
Notably, recursive calling makes it impossible to set an upper-bound on gas limits and can lead to gas limit attacks. Additionally, the removal of modifiers was done with auditability in mind, as they can make code misleading and difficult to interpret from a human-readable perspective.
Vyper strips itself of security-vulnerable features but also adds some key functionality including bounds and overflow checking, decidability, and strong typing. In regards to gas limits, decidability allows a developer to compute a precise upper-bound for the gas consumption of a function call.
A major distinction between Vyper and Solidity is that — although they look similar — Vyper removes much of the object-oriented archetypes present in Solidity. The emphasis on simplicity for Vyper also enables it to be much more readable in instances where auditing by parties not very familiar with programming are necessary. The potential use of Vyper is, therefore, appealing to many practical business dapps that can be written in Vyper.
Security considerations at the programming language level are important to take into account. Simplicity often leads to less required logical complexity and can inherently provide better security. Vyper is also not necessarily designed to replace Solidity, rather it is built to provide a simpler and more secure language as an alternative option for when it is necessary.
Scilla is an intermediate-level smart contract language used by Zilliqa. Scilla is explicitly designed with security and smart contract safety in mind. Importantly, it focuses on providing formal verification of smart contracts.
Formal verification is designed to provide static guarantees of smart contracts before they are immutably committed to the blockchain. Formal verification of smart contracts is becoming more prevalent in the field and is actively being pursued and applied by several platforms including Tezos and Cardano. The use of formal verification should substantially reduce instances of buggy code committed to blockchains and subsequently lower the need for intensive smart contract auditing by third-parties.
Scilla is carefully designed to be expressive enough to build useful dapps, while still ensuring the formal reasoning about contract behavior. Similar to Vyper, the primary principle is simplicity and security over expressiveness. An important distinction that needs to be made about Scilla though is that is an intermediate-level language, meaning it is intended to be a translation target for high-level languages and subsequently compile down into executable bytecode. As a result, the language is more challenging to understand than a high-level language like Solidity.
Scilla separates communication and computation, which has significant consequences for how contracts are executed. Contracts are structured as communicating automata where in-contract computations are executed as atomic transitions without involving any other parties. Moreover, an instance of required involvement by another party results in an explicitly communicated end to the transition. Contract-specific effects such as transitions can then be decoupled from blockchain interactions like messages and sending/receiving funds.
Additionally, Scilla provides separation between effectful and pure computations along with separation between invocation and continuation. Regarding effectful and pure computations, Scilla draws inspiration from functional programming citing:
“By carefully designing semantics of interaction between pure and impure language aspects, we ensure a number of foundational properties about contract transitions, such as progress and type preservation, while also making them amenable to interactive and/or automatic verification with standalone tools”
The separation of invocation and continuation refers to structuring contracts as communicating automata to provide a CPS computational model. Using this model with explicit continuations, languages like Solidity can be translated directly to Scilla without compromising the integrity of the automata structure.
The formal verification component of Scilla is enabled by its embedding into the Coq Proof Assistant, a formal proof management system designed to provide mechanically verified proofs of smart contracts and distributed applications. The result is the formal verification of contracts that reason about both the properties of safety and liveness. Correctness in distributed systems can be separated into safety and liveness. According to Zilliqa:
Safety is when “nothing goes wrong” – This is a guarantee that something bad will never happen. In consensus, this is when no two processes decide on different values. Another example would be that there is no deadlock in distributed transaction systems. Safety has important consequences on the overall integrity of smart contracts in the long-term.
Liveness is where “certain things may eventually happen” – A guarantee that something good will eventually happen. The word “eventually” also does not imply a time bound but if the system runs long enough, then liveness is guaranteed. For instance, in consensus, all processes will eventually decide on a value. Another example is the completeness of failure detectors that will eventually detect faulty processes.
Zilliqa’s development of Scilla parallel with formalization and its embedding in Coq should prove a valuable decision for the future safety of smart contracts that run on its high-throughput blockchain.
Finally, Scilla is blockchain-agnostic and can be used for other blockchains. However, it is still under active research and development, primarily with the Zilliqa team. The Scilla website also provides a tutorial and Online IDE for trying out the language.
The continued innovation in smart contract development will assuredly see the rise of more contract-oriented programming languages and solutions to tackle their security. The need for security of dapps and smart contracts is of the utmost importance considering the amounts of value that are transferred over large cryptocurrency networks like Ethereum.
Initial iterations of smart contracts showed significant potential in their future capabilities. Now, a new class of developments is focused on improving their security at the programming language level to ensure their sustainability.