Debugging Smart Contract Programming Languages

Exploring how Solidity, DeepSEA, and Move languages differ, some pros and cons offered by each, and what to expect as more programmers enter Web3 development.

Following the introduction of blockchain technology cryptocurrency more broadly in the form of Bitcoin, Ethereum’s blockchain later introduced smart contract functionality as an added feature. Essentially this meant that developers could write more complex transaction logic into their code. This was made possible by implementing a new, Turing-complete programming language called Solidity.

In the years since, there have been implementations of several different programming languages in deploying blockchain applications. Rust, of course, has been a shining example of an incredibly fast and memory-efficient language, and the language of Solana’s blockchain. JavaScript, Go, Scala, Vyper, Yul, and Haskell are but a few of many other examples of programming languages commonly used by dApp developers. 

The following is a brief explanation and comparison of the programming languages Solidity, DeepSEA, and Move. To wrap up, we will attempt to distill the most relevant advantages and complications of each and provide insights for aspiring Web3 developers.

Solidity: The Original Smart Contracts Language

Solidity has become one of the most commonly used languages for writing smart contracts and the deployment of blockchain applications. Of course, it first gained prominence through its ubiquitous use by developers working within the Ethereum blockchain’s ecosystem. As Ethereum has exploded with popularity, so too has Solidity become a common tool in the typical Web3 developer’s repertoire.

The simplest, and perhaps most common application of Solidity by developers was for the creation of their own cryptocurrencies or tokens. On Ethereum, these tokens are created according to what has been named the ERC-20 standard. ERC-20 tokens are compatible with any application written on Ethereum’s blockchain. By using a universal standard within the Ethereum ecosystem, developers can be sure that their protocols and the tokens they create will be easily transferred between Ethereum user wallets.

The language has influences from both Python, JavaScript, and c++, resulting in a number of familiar features. For instance, Solidity is a curly-bracket language and supports inheritance, a core concept of object-oriented programming (OOP) languages. Consequently, developers learning Solidity should encounter an easier learning curve with prior knowledge of either JS or c++. 

Since Solidity was designed specifically for writing smart contracts, the language has very clearly defined functions and commands. Developers can also easily access timestamps for particular blocks and index wallet addresses on relevant blockchains. The simplicity of Solidity’s commands, its extensive libraries, and its orientation towards smart contracts make dApp development a much simpler and seamless experience, particularly for new developers entering the Web3 space.

An illustration of the infamous 2016 DAO re-entrancy attack. A user initiates several transfers without actually submitting them. The network confirms that the submitting account holds enough Ether for each transaction. The user then submits all transactions simultaneously, exceeding the amount of actual Ether in their wallet.

As previously mentioned, Solidity is a high-level, object-oriented programming (OOP) language. That is, its code is built around smart contracts as the ‘objects.’ Fundamentally, smart contracts are collections of code (functional) and data (state), residing at specific addresses on Ethereum’s blockchain. Smart contracts are the fundamental building blocks for application development on Ethereum and the Ethereum Virtual Machine (EVM). 

The EVM is a secure runtime environment for executing smart contracts on Ethereum’s network. Its purpose is to facilitate the execution of untrusted code, using a global network of public nodes.  Ethereum’s VM ensures effective communication is securely established and maintained, prevents denial-of-service attacks on the Mainnet, and ensures that protocols can’t manipulate code or access each other’s sensitive data aside from what’s already public.

Since the EVM compiles Solidity into its bytecode, any blockchain (i.e. Avalanche, Polygon, Solana, Binance, etc.) which makes use of the EVM can also run smart contracts originally developed in Solidity. Therefore, the interoperable potential of Solidity within the Web3 ecosystem provides endless opportunities for devs to scale their projects. 

Nevertheless, Solidity has several error-prone features worthy of criticism, though devs have been steady at work tightening up the screws when needed. For instance, number overflow can occur if they are allowed to get too large, but was mostly addressed in Solidity version 0.8. In addition, smart contracts written in Solidity may be vulnerable to re-entrancy attacks due to Solidity’s function call semantics, resulting in recursive double withdrawals. This exploit has been used to steal hundreds of millions of dollars worth of crypto, including $3.6m worth of Ether in the infamous DAO attack.

Solidity’s Optimizer was also found to have a significant bug (known as the ABIEncoderV2 bug), found through the Ethereum Foundation’s bug bounty program. While the bug never resulted in a major network exploit, the presence of a bug which emits incorrect bytecode could be catastrophic. Though Solidity is a robust and flexible programming language for writing smart contracts, its vulnerabilities require third parties to verify the functionality and security of the source code or underlying compilation into the EVM. 

Since devs interact with the source code written in Solidity, the underlying compiler would throw errors in a way which would make it difficult for developers to identify the problem. Consequently, these bug bounties and other auditing firms tasked with performing formal verification have emerged as solutions for ensuring source code correctness and security conditions, giving devs and users increased peace of mind. In Solidity’s case, its formal verification approach is based on SMT solving.

Solidity’s built-in SMT solver is another solution which addresses the verification of the source code. The SMT solver facilitates annotating a given function with a set of conditions, writing assertions that should hold, and asking the compiler for verification. However, the assertions are limited in their usefulness, not to mention that devs need to trust that the compiler itself has not become buggy over time. 

While it may be simple enough to develop software in Solidity that works as expected, it is much more difficult to anticipate the myriad of ways in which it could be misused or exploited for gain. Therefore, the size of Solidity’s developer community is rather significant, thanks in part to the popularity of Ethereum and its Foundation. That is to say, that with more developers working together to find and solve issues with the language and its implementations, the more robust its security and use cases become.

DeepSEA: An Emphasis on Formal Verification

DeepSEA, developed by professors of Columbia and Yale, is another programming language worthy of discussion. DeepSEA was formally released by CertiK. The language prioritizes intuitive Formal Verification within the language itself, automatically creating mathematical theorems to prove the code’s correctness. By enabling the expression of code correctness at various layers of abstraction, developers can more confidently and efficiently build higher-level features atop lower-level features.

Since DeepSEA was designed with specific security and Formal Verification measures in mind, it is highly appropriate for blockchain and other decentralized, self-executable programs. In an automated and deterministic world, even the slightest errors can lead to devastating losses. 

DeepSEA was the first language to support equational reasoning, abstraction refinement, layered specification, as well as effect encapsulation and composition. The DeepSEA compiler automatically outputs executable bytecode and a model program to be tested in a safe, Coq environment. This provides developers with a provably correct model of their written code, and could save time compared with using a third party for manual Formal Verification of the code. 

Perhaps the most significant differentiating factor of DeepSEA is that its compiler is written in Coq and with code correctness being intuitively verified. This ensures the high-level language’s semantics are preserved by the compiler’s bytecode without introducing hidden errors into the source code during compilation. In other words, the correctness proven in the Coq testing environment adds to the integrity of the code as it grows by allowing layered verification of its functionality. 

In addition, the compiler has a verified backend to generate EVM-compatible bytecode. Since the generated code is ABI-compatible with Solidity, smart contracts written in Solidity and DeepSEA can successfully call on each other. This is important given that blockchain interoperability has become a primary focus for Web3 firms, developers, and investors, so DeepSEA’s features may be particularly suited to address their needs.

Move: Libra’s Diem Legacy Lives On

At its white paper release, Facebook’s Diem blockchain revealed it was written in a novel, bespoke programming language called Move. The team announced that the language was intended to strike an appropriate balance between the source code’s expressivity (like creating resources) and security assurances. Despite Diem’s failure to launch, Move is an open-source language, and has garnered attention from developers looking for creative solutions to some of the most difficult challenges in Web3 development.

Compared with Solidity, Move has three key differences. First, Move omitted certain features like dynamic dispatch and general pointers, limiting Move’s expressivity. This was likely done to address the re-entrancy bugs suffered by Solidity and make Formal Verification more straightforward, but results in restricting the language’s overall flexibility. 

Secondly, Move supports resource types inspired by linear logic systems. Move explicitly credits Rust as inspiration for its use of resource types with move semantics as explicit representations of digital assets like cryptocurrencies, tokens, and NFTs. Thus, particular types of data can be designated to be resources, meaning that code outside the module can’t look into the contents of values of that type. Rather, they’re only permitted to be moved between variables and passed to functions, ensuring resources are conserved. That is, that the number of outstanding tokens can’t be manipulated or double spent.

Finally, in its implementation, the Move compiler first generates bytecode and then a verifier called Move Prover type-checks the output. This contrasts with Solidity’s compiler, which first type-checks the source code and then subsequently generates bytecode. Since Move type-checks the generated bytecode, it provides more confidence that safety properties will behave properly. Though Move’s bytecode verifier can confirm well-written code, it does not guarantee functionally correct execution of the program as written, and includes the risk that compiler bugs may still fail to detect unexpected behaviors.

Source: Diem

Move was clearly designed with Solidity’s shortcomings specifically in mind, and has successfully mitigated many of them, as mentioned. Its designers seem to have prioritized an easy learning curve as well in that its security and correctness can be easily verified via its Move Prover compiler. Though its code is more easily verified in comparison with code written in Solidity, it is arguably less elegant than DeepSEA’s integrated Formal Verification.

Having said that, Move has a few more similarities with DeepSEA. The languages are both disciplined, and limited in their flexibility compared to Solidity. Move has a tree-structured storage framework, meaning data locations are accessible through a single path. This, as mentioned, gives both Move and DeepSEA similar verification-friendly designs. 

Furthermore, Solana recently proposed using Move’s Virtual Machine as a means to more safely manage invocations between modules as the Move VM includes an advanced type system which runs these checks via its bytecode verifier. Since Move’s bytecode can be verified, the cost of verification is halved, since the module only charges fees once for recording it on chain.

Learning to Code: A Work in Progress

As the blockchain ecosystem continues to mature, new programming languages and Virtual Machines are likely to continue emerging to grapple with issues arising in the coming years. Though Solidity took first-mover’s advantage, newer languages like Move and DeepSEA have grown in popularity as they have attempted to address the shortcomings of Solidity from the outset of their design. Having said that, Solidity will continue to experience enhanced network effects from early adoption and the pervasiveness of Ethereum’s blockchain across the Web3 ecosystem. 

The good news is that each hack makes the system more resilient. We assume developers will learn from the mistakes of the past, and continue to improve Web3. Nevertheless, attacks are sure to increase as more capital flows into the crypto space, and could also become more complex in their ability to exploit attack vectors in the future. Developers need to always prioritize security over everything else in writing code, not to mention make ample use of security audits on an ongoing basis and proactively seek issues with bug bounties. As the old saying goes, “Rome wasn’t built in a day.”

References

1. Alt, L., Reitwiessner, C. (2018). SMT-based verification of Solidity smart contracts. In T. Margaria & B. Steffen (Eds.). Leveraging Applications of Formal Methods, Verification and Validation (pp. 376-388). ISoLA 2018.
2. Dams, D., & Grumberg, O. (2018). Abstraction and abstraction refinement. In E. Clarke, R. Henzinger, H. Veith, R. Bloem (Eds.) Handbook of Model Checking (pp. 385-419). Springer.
3. Dannen, C. (2017). Introducing Ethereum and Solidity. Apress.
4. Dill, D., Grieskamp, W., Park, J., Qadeer, S., Xu, M., Zhong, E. (2022). Fast and reliable formal verification of smart contracts with the Move Prover. In Fisman, D., Rosu, G. (Eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022 Conference Proceedings.
5. Iredale, G. (2021, 12 Aug.). An overview of Move programming language. 101 Blockchains. 
6. Gu, R., Koenig, J., Ramananandro T., Shao, Z., Wu, X., Weng, S., Zhang, H., & Guo, Y. (2015). Deep specifications and certified abstraction layers. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 50(1), 595–608.
7. Sjöberg, V., Sang, Y., Weng, S., & Shao, Z. (2019). DeepSEA: A language for certified system software. Proceedings of the ACM on Programming Languages, 3, 1-27.
8. Zeil, S. J. (2021, 14 Dec.). Turing completeness. Old Dominion University Computer Science CS390 Lecture Notes.
9. Zhong, J., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C., & Dill, D. (2020). The Move prover. In S. K. Lahiri and C. Wang (Eds.) Computer Aided Verification 2020 (pp. 137-150).

Related Articles

• What are Smart Contracts?
• Blockchain Programming Languages for Ambitious Web3 Developers
• Why is the Rust Language Skyrocketing in Popularity?

Learn More

• What is Decentralized Finance?
• A Critique of Existing DeFi Oracles
• What is DeFi Llama?