Move 是一种相对发展时间较短的编程语言，但已经在许多Web3.0 项目中得到了应用。

CertiK 安全专家团队最近审计了一个支持 Move 编写智能合约的新型 Layer 1 区块链。借此机会，我们将为大家整体概述一下Move 这一新型编程语言。

鉴于该内容较为专业，因此分为了（上）（下）两篇文章来进行讲述，在这篇文章中，我们将讨论 Move 及其两个特性：可编程资源（有助于支持高交易率）和形式化验证（有助于提高安全性）。

在这一过程中，本文也将展示 Move 的语法、类型系统和内存模型，并研究工程师在使用 Move 时可能犯的一些常见错误。除此之外，我们也将从技术角度审视 Move 形式化验证的潜力及面临的挑战。

什么是 Move？

Move 是一种用于编写智能合约的特定领域编程语言。最近推出的几个热门项目均支持 Move 语言，包括Aptos、0L 和 Starcoin 区块链。另外还有Sui 区块链同样支持 Move 语言并将其命名为 Sui Move。

Move 最初是作为Diem 项目的一部分开发的，但这一属于 Meta（原 Facebook）的基于区块链的支付网络现在已被解散。

在 Diem 发表的《为什么要创建 Move？》文档中，其指出“为了成功支持像 Diem 支付网络这样的支付系统，我们需要一种可以对数字资产的所有权进行编码，并为这些资产的转移创建程序的编程语言。目前已经有数百种语言在使用，其中一些已经作为原生语言包含到区块链的实现中。

Diem Networks 本可以选择一种通用语言，如 WebAssembly 或 Java 字节码，或现有的区块链语言，如 EVM 字节码或比特币 script。理论上，我们的确应当选择一种现有的语言，毕竟一种语言的社区、库、工具都和语言设计一样重要，而这些都需要多年的时间来建立。从这一角度上来说，应该谨慎创建一种新语言。但最终选择创建 Move 是因为我们看到了一个机会——Move 将可以帮助我们在几个重要方面对现有替代方案进行逐步改进。”

Diem 需要安全地支持大量的交易，因此其团队决定以这些目标为基础创建 Move。

可编程资源

Move 的关键特征之一是它对可编程资源的使用。一个资源（Resource）直接代表着一条有价值的数据（例如一个用户所持有的项目资产数量）。在 Move 中，每个持有项目资产的账户中通常都存储着可以直接代表该资产的数据。这与 Solidity 中项目资产的表示形成了鲜明的对比，从账户到他们持有的项目资产数量的映射，Solidity 通常是使用一张映射表在智能合约中进行记录。

这种对可编程资源的利用有两个主要优势。首先，它形成了一个支持高交易率的智能合约编程模型。如果一项交易涉及两个「仅相互交互」的账户，该交易可以与其他交易并行执行。

类似于现实生活中，小明在便利店结账付款并不影响小红的结账付款。Aptos 区块链就是一个很好的例子，其使用软件交易存储器来并行运行交易，并检测两个同时进行的交易是否可能发生冲突。

可编程资源的第二个优势是它们可以自动验证程序是否存在某些类型的错误：例如，资源永远不会被悄无声息地删除或复制——这是由 Move 编译器完成的。但是仍然有可能在智能合约代码中引入算术或逻辑错误，从而导致资源中出现不正确的值。

下图来自 GitHub（https://github.com/move-language/move）上的 Move 文档，显示了区块链数据在 Move 中的组织方式。Move 将区块链状态称为全局存储。

每个区块链地址代表一个账户，其中一些可能是外部拥有的。与以太坊不同的是，所有地址都可以存储数据。在下图中，BasicCoin 持有者的账户中有数据表明他们所持有的 BasicCoin 数量（资源）。该图显示，地址 0x42 还拥有一个实现 BasicCoin 的代码模块。

当使用 Move 编写智能合约时，最好的做法是将资源存储在拥有该资源的账户中，而非包含该智能合约代码的账户中。尽管有可能在 Move 智能合约中实现「Ethereum 风格」的资源映射，但涉及此类合约的交易可能无法并行执行。

Move 的安全功能

Move 包含几个可帮助开发者创建更安全智能合约的功能。其中就包括上文所提到的“编译器会检查资源的基本使用情况”这一功能。Move 语言原生就支持形式化验证，并有意排除了那些容易导致形式化验证困难的语言结构。

此外，Move 还支持泛型。泛型编程（Generic Programming）允许通用代码在不同类型中被重复使用。

这一点很重要，因为使代码更安全的一种方法是重用那些已被专家精心编写过的代码，少编写一些新代码。就像许多 Coin 共享实现代码——如 Aptos Coin 标准所示，通用编程允许该代码在不同 Coin 之间共享。

Move 类型系统和 Rust

在处理有价值的数据时，追踪清楚是谁拥有这些数据，并限制对这些数据的操作（如复制或删除）十分重要。

幸运的是，已经有一种开发完善的支持所有权特性的编程语言：Rust。Move 的开发者在类型和语法方面都受到了 Rust 思想的启发。

此图表显示了 Move 的内置原始类型：

此图表显示了 Move 的结构类型，这些是由其他类型构建的类型：

当涉及到结构类型时，事情就变得有趣了，结构类型是 Move 中唯一的用户定义类型，一个结构类型是一个存储在字段中的值的集合：

在 Move 中，结构是一种“value”类型。结构类型的 value 在内存或存储中是线性排列的，对一个结构的引用必须明确地构建。这与 Solidity 不同，在 Solidity 中，结构变量通常是对底层value的引用。下图说明了这一点：

字段可以是除引用类型之外的任何类型，结构的实例是通过打包创建的（就像在 Rust 中那样）。

Move 为结构类型的 value 实现了一个类似于 Rust 的所有权系统，其中每个 value 都由包含它的变量或字段拥有。引用并不拥有它们所指向的任何 value。

默认情况下，结构value只能被转移到另一个所有者，它们不能被复制或删除。当一个结构value被转移到另一个所有者那里时，它将无法被先前的所有者访问。

在一个结构类型的value被创建后，同一时间只存在该value的一个可以使用的副本。以下代码说明了这一点：

Move 还有一个称为abilities的类型特性，它可以控制一个给定类型的value 可被允许进行哪些操作——这是受到了 Rust 的启发。这四种能力分别是：

Copy：value 可以被复制。不具备复制能力的结构在被使用后无法被访问。

Drop：value 可以被删除。当一个 value 的所属变量或字段超出范围时，该 value 将被删除。不具备删除能力的结构则必须被使用，无法被丢弃。要么明确地销毁它们，要么将它们“转移”到其他地方。它们不能被无声无息地删除或丢弃。

Store：value 可以存储在全局存储的其他结构中。

Key：该类型可用作「键」来对全局存储进行访问。

对于结构类型来说，abilities是在结构类型声明中声明的，如下图所示：

（上）篇结语

上文内容主要介绍了 Move 是什么，以及其的一个关键特性:可编程资源。

我们希望这一内容介绍可以为那些对 Move 编程语言感兴趣的读者开拓一些思考方向。在（下）篇中，我们将继续介绍Move 的另一关键特性：形式化验证。欢迎各位读者持续关注。