The language of money, Part one: Why build Move?

Move is the open source programming language built for digital assets. The Language of Money series will explore its application and benefits. Part One introduces the principles of Move and its design philosophy.

Introducing Move

To successfully support a payment system like the Diem Payment Network, we need a programming language that can encode ownership of digital assets and create procedures for the transfer of those assets. There are hundreds of languages already in use, some of which are already native to blockchain implementations. Diem Networks could have chosen a general-purpose language like WebAssembly or Java bytecode, or an existing blockchain language like EVM bytecode or Bitcoin script. Typically, choosing an existing language is the right decision. The community, libraries, and tooling for a language is at least as important as the language design, and each of these takes years to build.

Thus, the decision to create a new language should not be taken lightly. We chose to create Move because we saw an opportunity to create a step-change improvement over existing alternatives in several important ways. In this post, we will explain the role and requirements of a blockchain language and show how Move’s design solves several problems with existing approaches.

The role of a language

In any blockchain, the role of the chosen language is to provide accurate representations of state and transition:

State:
What is the value of an asset?
Where is the asset stored?
Who has ownership of the asset?

Transition:
Who can create/destroy/move assets?
What state transitions are allowed?
What are the rules for transferring assets?

Requirements of a blockchain

For any programming language to be suitable for blockchain use, it must be deterministic, hermetic, and metered:

Deterministic
A blockchain uses an SMR (state machine replication) approach, wherein different entities in the network called validator nodes accept transactions from users and then refer to a set of transaction execution rules to update their internal state.

To execute that transitioned state and ensure that all other validators replicate it, the network follows a consensus protocol. Consensus is formed when the validators have the same starting state, agree on the next transaction, and produce a deterministic state transition as the result of the transaction. The current state is then updated across all validators.

If determinism cannot be ensured, validators will be unable to achieve consensus and the network will fail to make progress.

This requirement eliminates many general-purpose programming languages from use in a blockchain. In the case of C, for example, the lack of memory safety is untenable, while a language like Java allows for operations with undefined semantics – making either of these unsuitable for safely expressing state transitions for the SMR approach.

Hermetic
Due to the necessity of maintaining fidelity on the blockchain, it is vital that the inputs to transaction execution are strictly limited. In the case of a blockchain, programs must only be allowed to accept inputs from the global state or the current transaction. Any reference to an external source (e.g., reading from the filesystem or accessing a network) jeopardizes the ability to form consensus by presenting the possibility for returning differing values for different validators.

Most programming languages have features with nondeterministic semantics or use standard libraries that implement essential utilities with non-deterministic behavior for accessing the environment.

Metered
To ensure that the network continues to process transactions, each state transition must be assigned an upper bound on resource consumption. Without defined bounds, the network may stall in the presence of long-running or even non-terminating transactions.

This is the impetus for the gas function in many blockchains, which limits the runtime of each individual program and terminates if the limit is breached. This metering functionality is almost never a built-in component of general-purpose languages, and consequently disqualifies the majority from use in a state machine replication application. Note that metering based on wall-clock time is not suitable because it may introduce nondeterminism.

Understanding the properties of Move

We built Move to preserve simplicity while supporting the complex needs of a global financial infrastructure by striking a proper balance between the expressivity of the source language (e.g., creating resources) and safety measures. In order to provide accurate representations of states and transitions at such tremendous scale, we have made a number of adjustments to the paradigms of other languages with the addition of first-class resources, improved safety, and upgraded verifiability:

First-Class Resources
To address the problem of indirect representation, we introduce resources, a customizable type inspired by linear logic. Resources provide inherent scarcity protections: they can only ever be moved between program storage locations, never copied or implicitly discarded. Move’s type system provides static enforcement of these safety measures, but allows programmers to define custom resource types. Resources are ordinary program values that can be stored in data structures passed into/out of procedures without violating the safety measures.

By integrating resources at the type level rather than supporting a single kind of resource value (e.g., Ether), Move provides programmers with the security measures they need while remaining blockchain-agnostic. Any developer can instantly reap these benefits in custom assets, without the additional reimplementation process required by ERC20 (Ethereum Request for Comment, proposal 20) and others.

To protect the critical operations of resources from untrusted code, Move encapsulates the fields of each resource in a corresponding module. Modules are similar to smart contracts – they contain the types and procedures for creating, updating, and destroying its contained resources. They also provide critical data abstraction: the fields of a declared resource type within a module are shielded from any other module, and operations on that resource must be performed exclusively within its module.

Safety
The majority of existing blockchain languages are created as a source language, which is then compiled into bytecode where it is checked and verified before execution. This language flow provides a number of safety guarantees. But it also presents possible vulnerabilities: by including compilation in the trusted computing base, these languages mutate the compiler into an imperfect gatekeeper. In other words, a bad actor could bypass the source language and write malicious bytecode directly, thus introducing it to the execution environment without ever running through the compiler and verifying steps.

To avoid this, the executable format of Move is bytecode, and all of the necessary protections are encoded after the point of compilation. Move still retains a source language, but rather than embedding the safety guarantees into what will eventually be run through the compiler, the Move source language compiles to bytecode before being checked by a bytecode verifier and then executed directly by a bytecode interpreter. By removing the compiler from the trusted base, Move eliminates a possible point of subversion.

Verifiability
Move enforces safety properties in two distinct ways, depending on the property being checked.

Some safety properties, such as type, memory and resource safety, are universal across any Move program. These properties are verified and enforced on-chain via Move’s bytecode verifier.

Other safety properties are specific to the Move program being written. For example, an auction concludes with a single winner, or a crowdfunding campaign sends money to the funder or returns money to the investors. depending on whether the campaign succeeds or fails. These safety properties cannot be enforced on-chain since there is no way to know exactly what to verify since every program is unique. To solve this issue, Move has been designed to support functional verification, which allows a formal tool (the Move Prover) to provide verification against specification definitions provided by the specific Move program.

There are several design decisions Move has made in the interest of facilitating functional verification. Move eliminates dynamic dispatch and enables the target of each call site to be statically determined, which in turn improves the ability of verification tools to determine the effects of a procedure call.

Move has limited mutability and enhanced modularity. Move values can only be changed through references, which are limited to the confines of each individual transaction. In addition to improving the distinction between sharing and ownership between transacting parties, references also confine the global storage to a tree rather than an arbitrary graph and allows off-chain tools to more accurately reason and determine the effects of a write operation. We will revisit Blockchain languages in more detail in upcoming segments.

Next up in the series will explore money as a language feature.

Learn more

The Move language is open-source and entirely platform-agnostic.

On December 1st, 2020, Move documentation became publicly available for the first time on the Diem developer website. Any developer interested in improving the functionality and security of a blockchain is invited to build with Move, and use cases from all industries and applications are welcome.

To get started now, visit the Move documentation site to understand modules and scripts and then work through the first tutorial on creating coins.