Ethereum’s programming language, Solidity, has quickly become one of the most commonly used languages across the blockchain: its flexibility of purpose across Ethereum has led to rapid and widespread adoption by the community, despite shortcomings in intuitiveness and security.

With Facebook’s announcement of Libra, a global currency aimed at empowering billions of people, many eyes have begun analyzing Move, its programming language.

Another programming language, DeepSEA, was developed by CertiK and the research laboratories of Columbia University and Yale University. DeepSEA, which was awarded research grants from The Columbia-IBM Blockchain Center and The Ethereum Foundation, focuses on intuitively leveraging Formal Verification within the language itself, automatically creating mathematical theorems to prove code correctness.

Below, we compare Facebook’s Move with Ethereum’s Solidity and CertiK’s DeepSEA to interpret the differences between the languages, detailing the advantages — and complications — therein.

Solidity

Ethereum introduced the idea of smart contracts: while Bitcoin hardcoded the type of data stored on the blockchain, Ethereum allowed developers to customize a system by uploading arbitrary programs that can store any type of data and apply any kind of transaction logic. To implement these smart contracts, Ethereum leveraged a Turing-complete programming language called Solidity.

The simplest and most popular application of Solidity was to allow developers to create their own cryptocurrency (a “token”), which could be owned and transferred to any Ethereum account. Under the hood, tokens are created by simply uploading a program that stores a large table; this table states how many tokens each user owns (an integer), and exposes a few methods, e.g. the ability to transfer tokens from one account to another:

However, in practice, the Ethereum and Solidity experience has not been as smooth as expected. In many respects, the Solidity language has features that are unnecessarily error-prone.

For example, numbers can silently overflow if they get too large, exposing the programs to undesirable manipulations. More subtly, the Solidity method call semantics also allow for a vulnerability called a re-entrancy attack, in which contracts are able to be withdrawn twice in a recursive manner. This simple trick was used to exploit Solidity contracts in the past, leading to the theft of hundreds of millions of dollars, including the infamous DAO attack.

Another area of exposure in Solidity and Ethereum is in the basic infrastructure. So far, no particular high-profile failure has resulted from this, but there have been bugs found in the Solidity compiler which can lead to insecure contracts (see here). Normally a programmer only interacts with the source code of a program, so if the underlying compiler itself has a bug that emits incorrect bytecode, it would be nearly impossible to catch.

Even with thorough manual testing and static analysis, these opaque issues may still linger. For that reason, Formal Verification has emerged as the leading method of ensuring the correctness of source code.

Although Solidity does not inherently integrate with Formal Verification proof assistants, CertiK has developed a complex proof engine to take Solidity code and prove its correctness, securing it against severe vulnerabilities such as overflows and re-entrancy. While this serves as the most comprehensive method of auditing, it is still a multi-stage process to ensure security due to the framework of the Solidity language,

Overall, Solidity is a powerful and flexible language — but one still vulnerable to major errors. Solidity does not offer any features to prove the correctness of the code (or underlying compilation into the Ethereum virtual machine), so the most robust proof of correctness still requires third-party Formal Verification from CertiK.

Move

As Facebook enters the blockchain world with its Libra initiative, people are anxious to examine the code behind it.

While revealing the white paper of its cryptocurrency project, Facebook also introduced a new programming language, Move. Currently there is a single module called LibraAccount, which works like a token contract, but eventually there will be a way for third parties to write additional modules.

Compared to Solidity, the Move language is different in three key ways.

First, Move limits the expressivity of the language by omitting certain features, mainly dynamic dispatch and general pointers. This would quell the infamous re-entrancy bugs by restricting flexibility at large.

The Move designers claim that these restrictions will make it easier to write Formal Verification tools for Move in the future — these tools do not currently exist, but the Facebook team makes it evident that the team is aware of the advantages and importance of Formal Verification.

Under future work Facebook writes:

“We will create a logical specification language and automated formal verification tool that leverage Move’s verification-friendly design (see Section 3.4). The verification toolchain will check program-specific functional correctness properties that go beyond the safety guarantees enforced by the Move bytecode verifier (Section 5.2).”

Second, Move supports “resource types” (inspired by linear type systems). A module can declare a particular type of data to be a “resource,” which means that code outside the module cannot look into the contents of values of that type: they can only be moved between variables and passed to functions. This helps Move programmers make sure that resources are conserved, e.g. that the total number of outstanding tokens doesn’t change.

This type of system provides resource conservation guarantees that are generally useful, but they are not enough to ensure functional correctness — -and the Move designers agree.

Third, as a matter of implementation, the Move compiler generates typed bytecode, and a “bytecode verifier” performs a sanity check on the output. This is in contrast to the Solidity compiler which type-checks the source program first, and then processes it to generate bytecode.

By doing the type-checking last, Move can ensure the safety properties that are enforced by typing (in particular, conservation of resources) will hold. It is important to denote that this “bytecode verifier” serves as verification of a well-typed program, not a functionally correct program in and of itself. There can still be compiler bugs that cause a well-typed, but incorrect program.

Overall, the additional limitations of Facebook’s Move adds a layer of discipline that mitigates against the many avoidable vulnerabilities of Solidity. The aspects of security and correctness, however, are still treated as merely supplementary to the underlying language.

This is because the Move language slightly advances the programming standards by offering a “verification-friendly design.” This still requires the creation of additional tooling, however, as opposed to the more elegant DeepSEA approach of directly integrating Formal Verification into the language itself, allowing developers to work with their contracts in an interactive proof assistant (in this case, Coq).

DeepSEA

DeepSEA is a functional programming language that puts security first, using Formal Verification to secure code. By allowing a user to reason about a program (such as a smart contract) at a high level of abstraction, the process of determining correctness of code becomes seamless.

The DeepSEA compiler can automatically output two things for each program: first, an executable bytecode and second, a model of the program which can be loaded into Coq. This approach offers a general purpose theorem and proving environment that allows the addition of manually written specifications — offering flexibility and compatibility along security.

[An example of the DeepSEA to EVM compiler.]

DeepSEA has similarities with other languages: much like Move, the program model will be limited and disciplined, compared to Solidity. DeepSEA has the same “tree structured storage” that the Move paper discusses (every location is accessible under a single path), allowing it to have a similar “verification-friendly design.”

A major differentiation of the DeepSEA system from both Solidity and Move is that the DeepSEA compiler itself is written in Coq and proven correct. This means that, unlike basically all other systems, we can be certain that the semantics of the high-level language are preserved by the bytecode — and no new errors are introduced during the compilation. Whereas Move merely checks that the output of the code is well-typed, DeepSEA checks that the output is indeed correct (the correctness properties proven in the Coq model will be satisfied).

The DeepSEA language was designed to apply a significant level of protection beyond what other languages are able to provide. In a world in which the created systems are decentralized, self-executable, permanent, and open-source, even the most minor errors may lead to significant — and often costly — problems.

As a next-generation programming language, DeepSEA aims to apply the learnings of the past to lay the groundwork to create a more secure ecosystem for the future.

As the blockchain ecosystem continues to mature, new programming languages have emerged to counteract some of the known issues of the last few years. While the first-mover advantage allowed Solidity to experience heavy adoption and familiarity, new languages such as Move and DeepSEA are attempting to learn from — and prevent — some of the mishaps of the past.

Between the three, programmers have more options than ever to code as they see fit.

To learn more and get the latest updates about DeepSEA, check out our DeepSEA research page.