Move是一种相对发展时间较短的编程语言，但已经在许多Web.0项目中得到了应用。
CertiK安全专家团队最近审计了一个支持Move编写智能合约的新型Layer1区块链。借此机会，我们将为大家整体概述一下Move这一新型编程语言。
鉴于该内容较为专业，在这篇文章中，我们将讨论Move及其两个特性：可编程资源（有助于支持高交易率）和形式化验证（有助于提高安全性）。
在这一过程中，本文也将展示Move的语法、类型系统和内存模型，并研究工程师在使用Move时可能犯的一些常见错误。除此之外，我们也将从技术角度审视Move形式化验证的潜力及面临的挑战。
什么是Move？
Move是一种用于编写智能合约的特定领域编程语言。最近推出的几个热门项目均支持Move语言，包括Aptos、0L和Starcoin区块链。另外还有Sui区块链同样支持Move语言并将其命名为SuiMove。
Move最初是作为Diem项目的一部分开发的，但这一属于Meta（原Facebook）的基于区块链的支付网络现在已被解散。
在Diem发表的《为什么要创建Move？》文档中，其指出“为了成功支持像Diem支付网络这样的支付系统，我们需要一种可以对数字资产的所有权进行编码，并为这些资产的转移创建程序的编程语言。目前已经有数百种语言在使用，其中一些已经作为原生语言包含到区块链的实现中。
DiemNetworks本可以选择一种通用语言，如WebAssembly或Java字节码，或现有的区块链语言，如EVM字节码或比特币script。理论上，我们的确应当选择一种现有的语言，毕竟一种语言的社区、库、工具都和语言设计一样重要，而这些都需要多年的时间来建立。从这一角度上来说，应该谨慎创建一种新语言。但最终选择创建Move是因为我们看到了一个机会——Move将可以帮助我们在几个重要方面对现有替代方案进行逐步改进。”
Diem需要安全地支持大量的交易，因此其团队决定以这些目标为基础创建Move。
可编程资源
Move的关键特征之一是它对可编程资源的使用。一个资源（Resource）直接代表着一条有价值的数据（例如一个用户所持有的项目资产数量）。在Move中，每个持有项目资产的账户中通常都存储着可以直接代表该资产的数据。这与Solidity中项目资产的表示形成了鲜明的对比，从账户到他们持有的项目资产数量的映射，Solidity通常是使用一张映射表在智能合约中进行记录。
这种对可编程资源的利用有两个主要优势。首先，它形成了一个支持高交易率的智能合约编程模型。如果一项交易涉及两个「仅相互交互」的账户，该交易可以与其他交易并行执行。类似于现实生活中，小明在便利店结账付款并不影响小红的结账付款。Aptos区块链就是一个很好的例子，其使用软件交易存储器来并行运行交易，并检测两个同时进行的交易是否可能发生冲突。
可编程资源的第二个优势是它们可以自动验证程序是否存在某些类型的错误：例如，资源永远不会被悄无声息地删除或复制——这是由Move编译器完成的。但是仍然有可能在智能合约代码中引入算术或逻辑错误，从而导致资源中出现不正确的值。
下图来自GitHub（