在之前一篇关于人工智能的文章里，我指出了“自动编程”的不可能性。今天我想来谈谈一个相关的话题：智能合约的形式验证。有些人声称要实现基于“深度学习”的，自动的智能合约形式验证（formal verification），用于确保合约的正确性。然而今天我要告诉你的是，跟自动编程一样，完全自动的合约验证，也是不可能实现的。
随着区块链技术的愈演愈烈，很多人开始在以太坊的“智能合约语言”上做文章。其中一部分是搞 PL 的人，他们试图对 Solidity 之类语言写的智能合约进行形式验证，号称要用严密的数理逻辑方法，自动的验证智能合约的正确性。其中一种方法，是用“深度学习”，经过训练，自动生成 Hoare Logic 的“前条件”和“后条件”。
我好像已经把你搞糊涂了…… 我们先来科普一下 Hoare Logic。
Hoare Logic 是一种形式验证的方法，用于验证程序的正确性。它的做法是，先给代码标注一些“前条件”和“后条件”（pre-condition 和 post-condition），然后就可以进行逻辑推理，验证代码的某些基本属性，比如转账之后余额是正确的。
举一个很简单的 Hoare Logic 例子：
{x=0} x:=x+1 {x>0}
它的意思是，如果开头 x 等于 0，那么 x:=x+1 执行之后，x 应该大于 0。这里的前条件（pre-condition）是 x=0，后条件（post-condition）是 x > 0。如果 x 开头是零，执行 x:=x+1 之后，x 就会大于 0，所以这句代码就验证通过了。
Hoare Logic 的系统把所有这些前后条件和代码串接起来，经过逻辑推导验证，就可以作出这样的保证：在前条件满足的情况下，执行代码之后，后条件一定是成立的。如果所有这些条件都满足，系统就认为这是“正确的程序”。注意这里的所谓“正确”，完全是由人来决定的，系统并不知道“正确”是什么意思。
Hoare Logic 对于程序的安全性，确实可以起到一定的效果，它已经被应用到了一些实际的项目。比如微软 Windows 的驱动程序代码里面，有一种“安全标注语言”，叫做 SAL，其实就是 Hoare Logic 的一个实现。然而前条件和后条件是什么，你必须自己给代码加上标注，否则系统就不能工作。
比如上面的例子，系统如何知道我想要“x>0”这个性质呢？只有我自己把它写出来。所以要使用 Hoare Logic，必须在代码上标注很多的 pre-condtion 和 post-condition。这些条件要如何写，必须要深入理解程序语言和形式逻辑的原理。这个工作需要经过严格训练的专家来完成，而且需要很多的时间。
所以即使有了 Hoare Logic，程序验证也不是轻松的事情。于是呢就有人乘火打劫，提出一个类似减肥药的想法，声称他们要用“深度学习”，通过对已有标注的代码进行学习，最后让机器自动标注这些前后条件。还在“空想”阶段呢，却已经把“自动标注”作为自己的“优势”写进了白皮书：“我们的方法是自动的，其他的项目都是手动的……”
很可惜的是，“自动标注”其实跟“自动编程”是一样的空想。自动编程的难点在于机器没法知道你想要做什么。同理，自动标注的难点在于，机器没法知道你想要代码满足什么样的性质（property）。
除非你告诉它，机器永远无法知道函数参数必须满足什么样的条件（前条件），它也无法知道函数出口应该满足什么样的条件（后条件）。比如上面的那个例子，机器怎么知道你想要程序执行之后 x 大于零呢？除非你告诉它，它是不可能知道的。
你也许会问，深度学习难道不能帮上忙吗？想想吧…… 你可以给深度学习系统上千万行已经标注前后条件的代码。你可以把整个 Windows 系统，整个 Linux 系统，FireFox 的代码全都标注好，再加上一些战斗机，宇宙飞船的代码，输入深度学习系统进行“学习”。现在请问系统，我下面要写一个新的函数，你知道我想要做什么吗？你知道我希望它满足什么性质吗？你仍然不知道啊！只有我自己才知道：它是用来自动给我的猫铲屎的 :p
所以，利用深度学习自动标注 Hoare Logic 的前后条件，跟“自动编程”一样，是在试图实现“读心术”，那显然是不可能的。作为资深的 PL 和形式验证专家，这些人应该知道这是不可能自动实现的。他们提出这样的想法，并且把它作为相对于其他智能合约项目的优势，当然只是为了忽悠外行，为了发币圈钱 ;)
如果真能用深度学习生成前后条件，从而完全自动的验证程序的正确性，那么这种办法应该早就在形式验证领域炸锅了。每一个形式验证专家都希望能够完全自动的证明程序的正确性，然而他们早就知道那是不可能的。
设计语言来告诉机器我们想要什么，什么叫做“正确”，这本身就是 PL 专家和形式验证专家的工作。设计出了语言，我们还得依靠优秀的程序员来写这些代码，告诉机器我们想要做什么。我们得依靠优秀的安全专家，给代码加上前后条件标注，告诉机器什么叫做“正确安全的代码”…… 这一切都必须是人工完成的，无法靠机器自动完成。
说到这些，我就为这些学者感到悲哀，想不鄙视他们都不行了 :p 很早的时候我就有这种感觉，总是有些 PL 人看到什么方向有钱就往什么方向上靠，拿一堆吓人的术语来忽悠外行。管它一个外行设计的语言有多垃圾呢，我们帮它做形式验证工具，我们为它写编译器，写虚拟机，为它提出“形式化语义”（formal semantics）！给外行打下手，给母猪涂口红，完全失去作为一个专家的责任感和尊严。
现在这种风气愈演愈烈，随着比特币和以太坊的热门，他们开始在 Solidity 之类的语言和智能合约上做文章。新瓶子装老酒，反反复复做同样的事情。甚至完全失去职业道德，号称要实现一些早就知道不可能的事情。现在最热门的两个投资方向就是人工智能和区块链，现在我用机器学习来验证区块链智能合约的正确性，两个热点都占全了！;)
显然，我也可以轻而易举做出对智能合约进行某种“验证”或者“静态分析”的工具，然而我深刻的理解数理逻辑对于程序正确性的局限性。很多代码没法被证明为正确，但它们确实是正确的。很多代码有 bug，却没有任何工具可以发现它们。这是一个不幸的事实，就像无法实现永动机一样，没有任何人能够改变。
当然，我并没有排除对智能合约手动加上 Hoare Logic 标记这种做法的可行性，它是有一定价值的。我只是想提醒大家，这些标记必须是人工来写的，不可能自动产生。另外，虽然工具可以有一定的辅助作用，但如果写代码的人自己不小心，是无法保证程序完全正确的。
如何保证智能合约的正确呢？这跟保证程序的正确性是一样的问题。只有懂得如何写出干净简单的代码，进行严密的思考，才能写出正确的智能合约。关于如何写出干净，简单，严密可靠的代码，你可以参考我之前的一些文章。
做智能合约验证的工作也许能圈到钱，然而却是非常枯燥而没有成就感的。为此我拒绝了好几个有关区块链的合作项目。虽然我对区块链的其它一些想法（比如去中心化的共识机制）是感兴趣的，我对智能合约的正确性验证一点都不看好。
实际上，我认为智能合约这整个概念就不靠谱。比特币和以太坊的系统里面，根本就不应该，而且没必要存在脚本语言。我认为智能合约系统在当前阶段并不可行。
比特币的解锁脚本执行方式，一开头就有个低级错误，导致 injection 安全漏洞。用户可以写出恶意代码，导致节点的运行时系统出错。我不可想象，在 2009 年仍然有人把两段代码以文本方式贴在一起，然后执行。稍微有点经验的黑客都知道这里很可能有可攻击的点。
以太坊的 Solidity 语言一开头就有低级错误，导致价值五千万美元的以太币被盗。以太坊的智能合约系统消耗大量的计算资源，还导致了严重的性能问题。可以说比特币和以太坊的作者都是 PL 外行，然而如果是内行来做这些语言，难道就会更好吗？我并不这么认为。
如果换做是我设计了比特币，我不会为它设计一种语言。让用户可以编程是很危险的！不仅是因为极少的用户能够写出正确而可靠的代码，而且因为语言系统的实现极少可以不出现 bug。语言系统的设计错误，会给黑客可乘之机，写出恶意脚本来进行破坏。从来没有任何语言和他们的编译器，运行时系统是一开头就正确的，都需要很多年才能稳定下来。另外一旦你让系统来运行这些语言的代码，又会需要考虑性能的问题。这对于普通的语言问题不大，你不要用它来控制飞机就可以。然而电子货币系统的语言，几乎不允许出现这方面的问题。
所以与其提心吊胆的设计这些智能合约语言，还不如干脆不要这种功能。
而且我们真的需要那些脚本的功能吗？比特币虽然有脚本语言，可是常用的脚本其实只有不超过 5 个，直接 hard code 进去就可以了。以太坊的白皮书虽然做了那么多的应用展望，EVM 上出现过什么有价值的应用吗？我并不觉得我们需要这些智能合约。电子货币只要做好一件事，能被安全高效的当成钱用，就已经不错了。
美元，人民币，黄金…… 它们有合约的功能吗？没有。为什么电子货币一定要捆绑这种功能呢？我觉得这是不够模块化的设计。电子货币就应该像货币一样，能够实现转账交换的简单功能就可以了。合约应该是另外单独的系统，不应该跟货币捆绑在一起。
那合约怎么办呢？交给律师和会计去办 :) 你有没有想过，为什么世界上的法律系统不是程序控制自动执行的呢？为什么我们需要律师和法官，而不只是机器人？这不只是历史遗留问题。需要理解法律的本质属性才会明白，完全不通过人来进行的机械化执法是不可行的。
奢望过多的功能其实是一种过度工程（over-engineering）。花费精力去折腾智能合约系统，将会大大的延缓电子货币真正被世界接受。实话说嘛，试用了多种电子货币之后，我发现它们的技术相当有趣，但其实仍然处于玩具和试验阶段，基本无法作为货币使用。绝大部分电子货币都在等着被淘汰。它们的发展方向存在着各种迷茫，很多人走向歧途，或者各种忽悠。
这篇文章可能对于比特币，区块链方向的投资者有很大的价值。如果我拯救了你的投资，欢迎你给我付费支持，一个 BTC 就可以 ;)
另外，我对于区块链技术还有挺多可以研究可以写的，好的不好的方面都有。甚至也许将来可以变成一本书。如果你觉得有收获，希望我继续发布这方面的内容，也可以付款鼓励一下，也欢迎联系我讨论你的看法。