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的另一關鍵特性：形式化驗證。歡迎各位讀者持續關注。

鄭重聲明：本文版權歸原作者所有，轉載文章僅為傳播信息之目的，不構成任何投資建議，如有侵權行為，請第一時間聯絡我們修改或刪除，多謝。