Facebook 發起的加密貨幣項目 Libra 6月18日正式公開亮相。Libra 同步發布了多語言官網和白皮書，定位為面向數十億人的全球貨幣和金融服務基礎設施。Libra 還發布了多個技術白皮書，詳細介紹了其新開發的編程語言 Move 和共識協議 LibraBFT。Libra 原始碼已在 GitHub 開源，測試網路也已上線。目前設計為許可鏈（聯盟鏈），其聲稱當前非許可鏈（公鏈）不存在成熟的解決方案能夠支撐數十億人的使用需求，並表明將在發布五年內開始轉向非許可鏈的過渡工作。
Libra 的一系列發布中，新的編程語言 Move 尤為吸人眼球。第一時間看了 Move 的白皮書，嗯，這也許才是未來智慧合約語言該有的樣子。
強悍的模塊系統
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，想了想，大概有下面三個原因：
- 汲取了 PL (程式語言)領域研究成果，同時也吸收了 EVM 智慧合約語言的經驗教訓
- 從設計上無比重視「智慧合約安全性、正確性」
- 沒有墨守成規（既沒有用WASM、LLVM，也沒有在 EVM 上直接修改），而是積極創新，是設計構思真正適合金融應用的智慧合約語言
本文為巴比特資訊授權刊登，原文標題為「Move語言：我眼中的 Libra 最大亮點」