10 年前，中本聪打开了加密货币的潘多拉之盒，在创世区块中摘抄了当天泰晤士报的标题，「The Times 03/Jan/2009 Chancellor on brink of second bailout for banks」。那个时候，他是否会想象到，在 10 年后的今天，世界已经发生了如此多的深刻的变化了。

Facebook 如期上线了 FBCoin 的 官网 和 白皮书（中译），官宣 里还放了几个钱包的截图，可谓吊足了人们的胃口。坊间已经有了各种讨论了，各种阴谋论也紧随其后。这里还是推荐 Binance Research 的调研报告和 孟岩老师 的访谈。

这一次同时上线的还有一个开发者网站，里面有三篇 Technical Papers，分别是：

• The Libra Blockchain 介绍 Libra Protocol 以及她的官方实现 Libra Core。
• Move: A Language With Programmable Resources 介绍为 Libra 量身定做的 智能合约语言 —— Move 语言。
• State Machine Replication in the Libra Blockchain 介绍 Libra 上跑的共识算法 —— LibraBFT。

之前就在想 FBCoin 的诞生如果要给开放式金融提供新的可能，就一定要看 FBCoin 赋予了开发者哪些权限，会不会推出自己的智能合约语言。这个想法现在得到了证实，这个语言直接被命名为 Move，一如 Facebook 的格言「Move Fast and Break Things」。同时 Move 也表示智能合约的本质就是对用户资产的转移（Move）进行编程，还真是一语双关呢。

初看 FBCoin 的白皮书和官网，特别是首页的那个宣传视频，里面反复的在各种普通人的生活日常中快速的切换着 —— 大多是还是来自我们这些第三世界国家 —— 这让我产生了一种非常不真实的穿越感，看来币圈还真的是一个有 时间膨胀 效应的地方。

但是无论讲解，我们都要在这种不真实感中寻找真实。这三篇 Technical Papers 包含比我预想的还要多的 Good Stuff ，总之我吃的很饱。

李笑来：Facebook 又犯傻，用得着专门设计个 Move 语言吗？—— 巴比特，对于 Facebook 发币，行业大咖如此点评 f you’re writing a program that has to work very closely with a program written in a certain language, it might be a good idea to write the new program in the same language.” —— Paul Graham

FBCoin 会推出自己的智能合约语言并不令人意外，毕竟上个月 Durov 在 TON 的 Channel 里就已经丢出了一份 Fift 的文档了 3。不出一个新语言，感觉扎克伯格在面子上也挂不住。另外 FBCoin 要处理的 Context 和我们目前所遇到的 Blockchain 都不一样 4，在 Move 的 Technical Paper 中这些诉求被归结为四点：

• First-class assets
• Flexibility
• Safety
• Verifiability

我们一个一个来看，先说安全性。和其他拥有自己的智能合约语言的区块链项目一样 5，Move 设计之初的一个核心诉求就是安全性，你能想象 Billions of People 因为一个智能合约的漏洞就被黑客攻击到损失惨重？—— 虽然我实际上相信 FBCoin 是可以回滚的 ……

In particular, transferring Ether to a smart contract involves dynamic dispatch, which has led to a new class of bugs known as re-entrancy vulnerabilities [16]. High-profile exploits, such as the DAO attack [17] and the Parity Wallet hack

[18], have allowed attackers to steal millions of dollars worth of cryptocurrency. —— Move: A Language With Programmable Resources

这里 Move 喜闻乐见的又把 Ethereum 上的这几个 Case 拿出来批判了一番。Move 的白皮书提到，想要一劳永逸的解决安全性的问题，不能信任智能合约的开发者，要么在编译期，要么在执行期一定要做检查。而 Move 看起来则是参考了 JVM 中的设计，选择了一个折衷主义的方案，在执行期之前，加了一个 Bytecode Verifier。

这是一组 PL 里的概念 6，所谓的编程语言中的一等公民就是在我们编程时首要考虑的被编程对象，最常见于理解各种函数式语言。

• First Class：该类型的值可以作为函数的参数和返回值，也可以赋给变量。
• Second Class：该类型的值可以作为函数的参数，但不能从函数返回，也不能赋给变量。
• Third Class：该类型的值作为函数参数也不行。

FBCoin 这里用这种说法，我认为只是在强调一件事情，就是用户自己发行的数字资产和 Libra 里的那个 StableCoin 是平级的。

这里原文还是继续 Challenge Ethereum。

However, the expressivity of the EVM has opened the door to expensive programming mistakes. Like StrawCoin, the Ether currency has a special status in the language and is implemented in a way that enforces scarcity. But implementers of custom assets (e.g., via the ERC20 [15] standard) do not inherit these protections (as described in (2)) — they must be careful not to introduce bugs that allow duplication, reuse, or loss of assets. This is challenging due to the combination of the indirect representation problem described in (1) and the highly dynamic behavior of the EVM.

一个典型的例子就是 美图币（BEC）。虽然这个 ICO 合约只在 OpenZeppelin 标准库的基础上增加了一个函数，结果那个函数里的操作就溢出了，使得黑客可以无限增发。类似的例子还有 POWH、Hexagon、etcs，不胜枚举。

另一方面，一些用户自己的代币不是第一公民，使得合约有的时候处理 Ether 和 ERC20 时，需要分别讨论。一个典型的例子就是 Bancor 的合约，为了避免额外的判断，Bancor 合约中单独写了一个 ERC20 Token 来打包 Ether，将相关的逻辑统一起来。后来这种方式逐渐形成标准，就是我们后来经常看到的 wETH 交易对。

这方面 EOS 的处理的则更为优雅，绝大部分底层的功能，也是通过超级节点部署智能合约的方式上线的，其中就包括 eosio.token 本身。而 EOS 和你自己发行的数字资产在合约里的唯一区别就是发行的合约不同而已，并且 EOS 的 assets 结构（还有 extended_assets），也已经包含了这些边界保护。

EOS 中是把原生资产和用户资产同时下放到了合约层面，而在 Libra 中，是把用户资产和原生资产同时上升到协议底层。

但是 Bytecode Verifier 理论上只能检查一下类型不匹配、内存溢出这样的简单 Bug，要检查出所有逻辑上的 Bug 无异说要解决 停机问题（Halting Problem），而且这部分时间复杂度也会被加到共识算法的 Critical Path 上，必须要做出相应的权衡。Move 的解决方法是，只将一些时间复杂度最低，同时又最关键的检查工作放在这个阶段，其他则寄希望于链下的静态验证的工具。

为了简化这些静态检查工具的设计，Move 在语言层面的功能上进行了一些必要的牺牲，而这一切都是为了将来做形式化验证做铺垫。

No dynamic dispatch

The target of each call site can be statically determined. This makes it easy for verification tools to reason precisely about the effects of a procedure call without performing a complex call graph construction analysis.

首先拿掉的就是动态分派。动态分派是指在运行期选择调用方法的实现的流程。现代高级编程语言中被广泛采用，被认为是面向对象语言的基本特性。但是一旦包含这个特性就会使得做静态验证十分困难。一个典型的例子就是 The DAO 硬分叉事件 [17] 里面的 Re-entrancy 攻击 [16]。

Limited mutability

Every mutation to a Move value occurs through a reference. References are temporary values that must be created and destroyed within the confines of a single transaction script. Move’s bytecode verifier uses a “borrow checking” scheme similar to Rust to ensure that at most one mutable reference to a value exists at any point in time. In addition, the language ensures that global storage is always a tree instead of an arbitrary graph. This allows verification tools to modularize reasoning about the effects of a write operation.

函数式语言的一个基本特性就是 Immutability，这使得我们可以在执行函数之前就可以对程序的状态进行断言。但是保持纯粹的 Immutability 的话，编写业务逻辑势必会十分痛苦。Move 这里依然采取了折衷主义的办法，参考了 Rust 的实现，保证每个对象在任何阶段只有一个可修改的引用，这样静态验证时就只要 trace 一个目标。

Modularity

Move modules enforce data abstraction and localize critical operations on resources. The encapsulation enabled by a module combined with the protections enforced by the Move type system ensures that the properties established for a module’s types cannot be violated by code outside the module. We expect this design to enable exhaustive functional verification of important module invariants by looking at a module in isolation without considering its clients.

https://doc.rust-lang.org/1.30.0/book/first-edition/mutability.html

Module 也是函数式语言中的概念，原本的目标是达成接口与实现分离这个目的，从而实现各个模块分别开发，验证与编译。与 Class 最大的区别在于 Class 是动态的，而 Module 是静态的。

在 Move 里则是扩展了这个概念的意义，根据白皮书，Move 里的智能合约分为两类：

• Transaction Script：一组顺序执行的，可以包含 Module 调用的转账语句，通常是一次性的，不在账本里进行保存。
• Module：定义和某个资产相关的操作方法的集合。

换句话说，这个 Module 才是更接近我们一般认为的智能合约。但是我强烈猜测只有资产的发行方才能够定义 Module 到 Libra 中去，例如 Uber 可以在 Libra 中定义一个资产叫优惠券，可以 Claim、使用和转让，而 Spotify 可能可以在 Libra 中定义另一个资产，比如一首曲子或一部专辑，支持订阅、转让、购买和注销。

而一般的开发者和 Startup 很可能只能开发一些 Transaction Script，来给你的 App 和网站描述一些功能有限的业务逻辑。所以大概率那 25 个合作伙伴才是 Libra 里的一等公民。

灵活性 Flexibility

最后 Libra 的灵活性仅仅只是相对于 Bitcoin Script 而言的，我们一般开发者还是老实一点写 Transaction Script 好了。

讲解保证智能合约的正确呢？这跟保证程序的正确性是一样的问题。只有懂得讲解写出干净简单的代码，进行严密的思考，才能写出正确的智能合约。关于讲解写出干净，简单，严密可靠的代码，你可以参考我之前的一些文章。

做智能合约验证的工作也许能圈到钱，然而却是非常枯燥而没有成就感的。为此我拒绝了好几个有关区块链的合作项目。虽然我对区块链的其它一些想法（比如去中心化的共识机制）是感兴趣的，我对智能合约的正确性验证一点都不看好。 —— 垠神，智能合约和形式验证

怎么样，这一套听下来，是不是很像 Tezos？Tezos 设计了一种参考了 OCmal 语法的函数式语言 Liquidity 来编写合约。合约又会被首先编译成一个 Stack-based 的中间语言 Michelson，并使用了一个魔改出来的 Mi-Cho-Coq 工具，来跑形式化验证的 Framework。

但是形式化验证真的是解决智能合约安全性问题的银弹吗？对此我抱有反对意见。为了安全性问题而在表达性上做牺牲似乎有舍本逐末的嫌疑，而且我认为即便要跑形式化验证，也可以让开发者使用一个 Solidity 语言的子集，姑且称之为 XSolidity 来跑 7 （类比 XHTML） —— 当然我期待着自由市场来打我的脸。

To say something is something, but unlike the previous version of that something because its defining characteristics are different, is a bit like saying:

Unlike previous loaves of bread, which view the loaf of bread as a collectively baked set of ingredients, the Libra Loaf of Bread is a single ingredient structure that bakes the components sequentially over time. Facebook’s Libra: blockchain, but without the blocks or chain – Financial Times

越来越多的人开始注意到，Libra 事实上既没有 Blocks，也没有 Chain，只是使用了 PBFT 跑了一个分布式数据库而已。但是我们知道，实际上比特币所要面对的，是一个比拜占庭将军问题更加困难的场景，在比特币里你实际上是没有一个 Global-View 的。节点可以随时加入和离开，通讯路径也是不可靠的，节点必须持续进行发现新节点，和帮助其他节点启动的工作。每个节点都只包含一部分关于网络的信息，因而逻辑上更像是一个 Mesh Network8，

Libra 这样的数据结构，也能算是区块链吗？如果按照 ConsenSys 的说法，大概是会被冠上 「Libra might not be a Real Blockchain at All」9 的帽子的。Jameson Lopp 也直接在他的文章标题里给 Blockchain 加了引号。

Blockchain: A blockchain is a replicated state machine [4][5]. Replicators in the system are known as validators. Users of the system send transactions to validators. Each validator understands how to execute a transaction to transition its internal state machine from the current state to a new state.

Cryptocurrency: A digital currency that uses cryptography to verify and secure financial transactions.

但是从上面 Libra 给 Blockchain 和 Cryptocurrency 的定义来看，好像又没什么问题。所以为什么我们会感觉那么奇怪呢？

Fb coin looks like eth and btc had a baby and switched to bft with appointed nodes that they claim will eventually be elected dpos style. The utxo model and asset focused primitives is likely to heavily restrict its applications. The concept of backing it with other assets means it fails when those assets fail. In effect it’s a new central bank. Note I have only read half of the white paper so I reserve my right to change my analysis. —— Daniel Larimer

《精通比特币》 和 《精通以太坊》 的作者，Andreas M. Antonopoulos 为此事先专门做了 一期 QA 视频，来友们为什么自己认为 FBCoin 不是真正的 Crypto。在这期视频里，Andreas M. Antonopoulos 给了 Cryptocurrency 的五个支柱，它们分别是：