区块链正本清源 – 从计算机科学评看区块链的起源和发展

我先引别人的一句话，“以太坊上的智能合约既没有智能也不是合约。”用可编程的计算机语言来表达合约，就存在根本性的约束。譬如，合约写成代码后是“定死”了的，哪来的智能。要能随机应变的智能，必须事先考虑好各种变化的可能。而在现实世界中，再紧凑的合约也有预想不到考虑不周的时候，或者双方对合约的内容有不同认知。现实世界中合约各方还可以坐下来商量，修改合约。在以太坊上，这些修改和商议或者仲裁的功能怎么实现？

跟随着以太坊的智能合约被很多人满嘴跑火车的另外一个词就是图灵完整 (Turing Complete)，好像这是个什么伟大的功能。其实若要真的想做智能合约，图灵完整又是一个背道而驰的思路。为什么这么讲？设计过计算机程序设计语言的人都知道，一个程序语言的限制越少，功能越强，程序员越容易出错。譬如， 大家常用的 C 语言就是这样一个例子。它功能强，是因为它出身是系统级的语言，做操作系统用的，需要这么强大的灵活性。但是作为写应用程序的需求来说，可以说到处是陷阱。后来推出的 Java 语言，增加了很多限制，譬如 type safety 和 garbage collection，把很多程序员容易掉陷阱的地方都回避开了，因此成为企业级应用的首选语言。

回到区块链的智能合约这个问题。要想安全可靠地写合约，合约语言必须进 一步缩减功能，加入很多约束。跟律师打过交道的都知道，合同一般分类有范本的，律师从来不愿意从头起草，而是在范本的基础上写合约。这就是因为范本提供了很多约束条件，经历过时间的考验和不断的更新，不容易犯错误。律师的范本就类似高级程序语言设计中的 type 和 pattern。前段时间以太坊上的 DAO 出现被攻击的事件，就是因为合约代码中的错误。所以说，对于写智能合约的程序语言来说，少反而是多。另外，真正要设计一个智能合约的语言，恐怕从一开始就要考虑如何结合形式验证(formal verification) 技术来证明每个合约的正确性，把可证明性(verifiability 或 provability)设计到语言的结构内。