作者：郭宇

在區塊鏈

領域裡面，凡是套用傳統方法的方案，無一勝出，唯有創新才有未來。——郭宇

相信各位和我一樣，今天被 Facebook 刷爆朋友圈。

Facebook 發起的加密數字貨幣

項目 Libra 今天（6月18日）正式公開亮相。Libra 同步發布了多語言官網和白皮書，定位為面向數十億人的全球貨幣和金融服務基礎設施。Libra 還發布了多個技術白皮書，詳細介紹了其新開發的編程語言 Move 和共識協議 LibraBFT。Libra 源碼已在 GitHub 開源，測試網路也已上線。目前設計為許可鏈（聯盟鏈），其聲稱當前非許可鏈（公鏈）不存在成熟的解決方案能夠支撐數十億人的使用需求，並表明將在發布五年內開始轉向非許可鏈的過渡工作。

Libra 的一系列發布中，新的編程語言 Move 尤為吸人眼球。第一時間看了 Move 的白皮書，嗯，這也許才是未來智能合約

語言該有的樣子。

一位來自柏林的開發者 Lefteris Karapetsas 在社交平台上提出了自己的觀點：

Their design goals seem to overlap, or even aim to replace Ethereum?

他們的設計目標似乎有些重疊，或者甚至旨在代替以太坊？

PuzzleToLife.com 的創始人 CryptoPuzzleDream 認為：

I think "move" programming language released by $FB could be more interesting than libra

我認為FB發布的 「move」 語言比 libra 更有趣。

James Clark 是一名標準極客，他說：

Im usually pretty skeptical of anything related to cryptocurrency, but heres one piece of Libra that looks potentially interesting: a bytecode programming language called Move with semantics inspired by linear logic.

我通常對與加密貨幣相關的任何東西都表示懷疑，但是Libra 中有一部分看起來相當有趣：一個被稱為 Move 的位元組碼編程語言，其語義受線性邏輯的啟發。

而我腦子裡閃過是這樣一句話：

Move 是為「數字資產」而生的智能合約平台型語言

Move 語言的三大用處

  1. 發行數字貨幣，Token，和數字資產
  2. 靈活處理區塊鏈交易
  3. 驗證器（Validator）管理

自底向上的靜態類型系統

Move 採用的是靜態類型系統，類型系統本質上是一種邏輯約束。相比以太坊的智能合約語言來說要嚴格地多。現代的編程語言比如 Rust, Golang, Typescript，Haskell, Scala, OCaml 都不約而同採用了靜態類型系統，他們的優點是，很多編程低級錯誤都可以在編譯的時候發現，而不是拖到運行期才爆出 bug。

Well-typed programs never get stuck.

這是程序語言（PL）領域的一句黑話：一個類型無誤的代碼永遠不會跑飛。意思是，如果一段合約代碼經過了類型檢查，那麼可靠性會相當高。

Move 也沒有設計成一個 100% 靜態類型檢查的語言，那樣會降低實用性。 Move 提到了盡量讓類型檢查在編譯的時刻進行，而不是等部署到鏈上之後。當然有些類型檢查不得不放到運行期，但是仍然可以保證類型安全。

Move 有個非常好的設計思路是，從虛擬機開始就是靜態類型化的，然後往上是一個中間語言層，IR（Intermediate Representation），也是類型化的。將來，Move 上層將會提供更多的面向各種金融應用的高級語言，那些語言自然也是靜態類型，保證智能合約不再會發生非常低級的錯誤。

First-class Resources 理念

First-class Resources 這個詞相當的學術，中文翻譯過來叫 資源是一等公民，

這究竟什麼意思呢？所謂的編程語言的一等公民就是編程語言在編程的時候首要考慮的被編程對象。

那麼資源，Resources又是什麼呢？ 這也是一個很學術的名字。Resources是和Value相對應

的概念。Value是可以隨意拷貝的，而Resources只能被消耗，不能被拷貝。Resources就像可樂，你喝了一瓶就少了一瓶，而Value，就好比寫在本子上的英文單詞，每天早上都可以念一遍，念完他不會消失，如果你記住了，那就在腦子裡拷貝了一份。不僅你可以念，我也可以念，你可以背，我也可以背。

傳統的編程語言，包括以太坊智能合約語言中，對於數字資產的記賬是採用的 Value 方式，這會導致一個問題：記賬是有可能記錯的。事實上記錯賬的智能合約相當得多，比如 張三向李四轉賬，李四的賬戶多了10塊錢，但是張三的賬戶餘額卻沒改。過去兩年里的各種記賬漏洞甚至一度搞得大家已經對智能合約的未來喪失了信心。

Move 合約採用了一種吸收了傳統理論「線性邏輯」的類型，叫做資源類型。數字資產可以用「資源類型」來定義，這樣一來，數字資產就像資源一樣，滿足線性邏輯中的一些特性：

  1. 數字資產不能被複制
  2. 數字資產不能憑空消失

First-class Resources 的真正含義是 數字資產是一等公民，這句話可以引申出，Move 是為操作數字資產而生的智能合約語言。從技術角度講，數字資產可以作為合約的變數，數字資產可以存儲，可以賦值，可以作為函數/過程的參數，也可以作為函數/過程的返回值。而 Move 的靜態類型系統使得智能合約代碼能夠在編譯期，也就是部署前就可以通過編譯器檢查出絕大多數的資源使用錯誤。保證智能合約不再像以前那樣的脆弱不堪。

摘用白皮書摘要中的一句話：

First-class resources are a very general concept that programmers can use not only to implement safe digital assets but also to write correct business logic for wrapping assets and enforcing access control policies.

作為一等公民的資源是一種非常普遍的概念，程序員不僅可以用它實現安全的數字資產，同時也可以編寫正確的業務邏輯，實現正確的訪問控制策略。

合約安全性設計

Move 合約在設計時，充分考慮了安全性。首先 Move 完全不支持動態指派（Dynamic Dispatch）。好，我這裡解釋下什麼是 Dynamic Dispatch，通俗地說，這是一種非常靈活的語言機制。在程序裡面是可以寫很多的函數，或者過程，或者子程序。然後一個主程序可以來調用這些函數/過程/子程序，來分別完成不同的功能。如果程序在運行之前，我們就能知道它到底都調用了哪個函數，或者以某種順序調用很多函數，那麼這些函數調用是「靜態」的，如果在運行之前，我們不清楚某一步的函數調用究竟是調用了哪一個函數，直到程序運行的時候，通過觀察，我們才能知道的話，那麼這個函數調用被稱為是「動態」的。「動態」顯然要比「靜態」靈活的多。

但是靈活也意味著更容易出問題。現代很多編程語言都或多或少支持 動態指派，也就是從語言層面直接支持，比如面向對象語言中的「繼承」導致的「動態綁定」。動態特性是不利於程序的推理，更不利於形式化驗證（Formal verification），也更容易出安全問題。在以太坊智能合約設計中就存在許多「動態特性」，比如支持函數指針做參數，合約做參數，delegatecall等等。而在 Move 語言中，完全不支持任何形式的「動態指派」或者「動態特性」，所有的合約執行路徑都能在編譯的時候確定，然後可以進行非常充分的分析、驗證。

Move 合約在運行前都會經過一個位元組碼驗證器（Bytecode verifier）進行校驗，這個驗證器可以檢查出各種類型錯誤。同時位元組碼在解釋執行的時候，仍然是帶著類型，一邊運行，一邊檢查。

Move 語言對合約可修改變數進行了非常嚴格的限制，並且從 Rust 語言那邊偷師了一些設計理念。保證任何時刻只能由一個指針對可修改變數進行修改，這樣不會造成混亂。以太坊 Solidity 裡面，可以定義很多的指針指向同一個變數，如果代碼邏輯沒考慮清楚，就會很容易出問題。

與以太坊EVM平台相比，Move 模塊系統不支持循環遞歸依賴，完美解決合約重入漏洞（Re-entrancy）。

強悍的模塊系統

Move 模塊系統採用的是一種函數式編程語言（OCaml, Coq, SML）風格的設計，按照白皮書的說法：

Move modules are similar to smart contracts in other blockchain languages. …, However, modules enforce strong data abstraction — a type is transparent inside its declaring module and opaque outside of it.

模塊系統可以很好地將數字資產的概念打包封裝，對於數字資產的操作比如通過模塊的公開介面，並且在這個介面上可以做靈活的許可權控制。在寫以太坊智能合約的時候，以太坊上的 ERC20 Token 是作為一個合約而存在，而在 Move 語言中，一個 Token 可以被想像成一個箱子，被隨意像資源一樣傳遞，但是同時不會暴露箱子內部細節。同時模塊系統的抽象也完全基於它的靜態類型系統，並且類型安全性完全可以由智能合約虛擬機來檢查保證。

Move 的模塊系統為智能合約的形式化驗證提供了非常好的基礎，在模塊內部可以定義「不變式」。所謂的不變式是指對數字資產內部狀態的一個嚴格約束，這個約束可以為形式化驗證的自動化提供非常有價值的信息。而且，模塊系統的「不透明抽象」可以使形式化驗證工作變得模塊化，成本更低。在Move 模塊系統上編寫程序分析器，符號執行器也會簡單很多，因為經過抽象，可以把合約邏輯變得非常簡單，易推理。

面向未來的 Move 智能合約

Move 雖然看起來還略顯粗糙和稚嫩，但是這個方向仍然讓人激動人心，從 Move 語言層面可以看到 Facebook 的野心，是想做一個龐大的數字資產平台。這個角色本來是應該屬於以太坊。

我為什麼有點喜歡上了 Move，想了想，大概下面三個原因：

  1. 汲取了 PL (程序語言)領域研究成果，同時也吸收了 EVM 智能合約語言的經驗教訓
  2. 從設計上無比重視「智能合約安全性、正確性」
  3. 沒有墨守成規（既沒有用WASM，LLVM，也沒有在 EVM 上直接修改），而是積極創新，是設計構思真正適合金融應用的智能合約語言

推薦閱讀：

相关文章