（这是之前关于人工智能的文章里面的一节。由于它关系到我最近发现的一些现象，所以把它提取出来，扩展之后单独成文。）
有人听说我想创业，给我提出了一些“忽悠”的办法。他们说，既然你是程序语言专家，而现在人工智能（AI）又非常热，那你其实可以搞一个“自动编程系统”，号称可以自动生成程序，取代程序员的工作，节省许许多多的人力支出，这样就可以趁着“AI 热”拉到投资。
有人甚至把名字都给我想好了，叫“深度程序员”（DeepCoder = Deep Learning + Coder）。口号是：“有了 DeepCoder，不用 Top Coder！” 还有人给我指出了这方向最新的，吹得神乎其神的研究，比如微软的 Robust Fill……
我现在可以很简单的告诉你，自动编程是不可能实现的。微软的 Robust Fill 之类，全都是在扯淡。我对微软最近乘着 AI 热，各种煽风点火的做法，表示少许鄙视。不过微软的研究员也许知道这些东西的局限，只是国内小编在夸大它的功效吧。
你仔细看看他们举出的例子，就知道那是一个玩具问题。人给出少量例子，想要电脑完全正确的猜出他想做什么，那显然是不可能的。很简单的原因，例子不可能包含足够的信息，精确地表达人想要什么。最最简单的变换也许可以，然而只要多出那么一点点例外情况，你就完全没法猜出来他想干什么。就连人看到这些例子，都不知道另一个人想干什么，机器又如何知道？这根本就是想实现“读心术”。甚至人自己都可以是糊涂的，他根本不知道自己想干什么，机器又怎么猜得出来？所以这比读心术还要难！
对于如此弱智的问题，都不能 100% 正确的解决，遇到稍微有点逻辑的事情，就更没有希望了。论文最后还“高瞻远瞩”一下，提到要把这作法扩展到有“控制流”的情况，完全就是瞎扯。所以 RobustFill 所能做的，也就是让这种极其弱智的玩具问题，达到“接近 92% 的准确率”而已了。另外，这个 92% 是用什么标准算出来的，也很值得怀疑。
任何一个负责的程序语言专家都会告诉你，自动生成程序是根本不可能的事情。因为“读心术”是不可能实现的，所以要机器做事，人必须至少告诉机器自己“想要什么”，然而表达这个“想要什么”的难度，其实跟编程几乎是一样的。实际上程序员工作的本质，不就是在告诉电脑自己想要它干什么吗？最困难的工作（数据结构，算法，数据库系统）已经被固化到了库代码里面，然而表达“想要干什么”这个任务，是永远无法自动完成的，因为只有程序员自己才知道他想要什么，甚至他自己都要想很久，才知道自己想要什么……
有句话说得好：编程不过是一门失传的艺术的别名，这门艺术的名字叫做“思考”。没有任何机器可以代替人的思考，所以程序员是一种不可被机器取代的工作。虽然好的编程工具可以让程序员工作更加舒心和高效，任何试图取代程序员工作，节省编程劳力开销，克扣程序员待遇，试图把他们变成“可替换原件”的做法（比如 Agile，TDD），最终都会倒戈，使得雇主收到适得其反的后果。同样的原理也适用于其它的创造性工作：厨师，发型师，画家，……
所以别妄想自动编程了。节省程序员开销唯一的办法，是邀请优秀的程序员，尊重他们，给他们好的待遇，让他们开心安逸的生活和工作。同时，开掉那些满口“Agile”，“Scrum”，“TDD”，“软件工程”，光说不做的扯淡管理者，他们才是真正浪费公司资源，降低开发效率和软件质量的祸根。
最近由于比特币和以太坊很热门，很多人开始在以太坊的“智能合约语言”上做文章。其中一部分是搞 PL 的人，他们试图对 Solidity 之类语言写的智能合约进行形式验证（formal verification），号称要用数学的方法，自动的验证程序的正确性。
其中一种办法，是给代码的函数加上“前条件”和“后条件”（pre-condition 和 post-condition），这样就可以使用 Hoare Logic 的办法来证明一些代码的基本属性，比如转账之后余额是正确的。
虽然 Hoare Logic 并不能完全的保证程序的正确，它确实可以起到一定的效果。然而要使用 Hoare Logic，必须人工写上很多 pre-condtion 和 post-condition。这些条件要如何写，必须要很深入的理解程序语言和形式验证。这个工作必须有经过多年严格训练的专家来完成。
世界上可以完成这种工作的专家，是非常少的，他们要求的报酬，也会非常高。所以呢，这些提出这种验证想法的 PL 人，就提出一个想法，他们要用“深度学习”的方法，通过对手写的前后条件进行机器学习，自动的生成这些前后条件。他们把这种“自动加条件”的特性，作为自己相对于其他手动验证方法的优点。
很可惜的是，“自动加条件”这种做法，其实跟“自动编程”是一样的，它完全的符合我在上一节指出的特征。自动编程的难点在于机器没法知道你想要什么，而自动加条件的难度在于，机器没法知道程序应该满足什么样的“特性”（property）。除非你告诉它，机器永远没有办法知道一个进入函数的时候，参数必须满足什么样的条件。同理它也不可能知道你想要在函数的出口满足什么条件。
试图用深度学习加上前后条件，这是同样的试图实现“读心术”的做法。这是根本不可能的，而且作为资深的 PL 和形式验证专家，这些人应该知道这是不可能的！他们提出这样的想法，并且把它作为相对于其他智能合约项目的优势，显而易见只是为了发币圈钱 ;)
如果真能用深度学习生成前后条件，自动的验证程序的正确性，那么这种办法应该早就在形式验证领域出现了。每一个形式验证专家都希望能够自动的证明程序的正确性，然而他们早就知道那是不可能的。
我为这些学者感到悲哀。很早的时候我就有这种感觉，总是有些 PL 人看到什么方向有钱就往什么方向钻，管它语言有多垃圾呢，我们帮它做验证工具，我们为它写编译器，写虚拟机！完全没有作为一个专家的尊严。现在这种风气愈演愈烈，随着比特币和以太坊的热门，他们开始在 Solidity 之类的语言和智能合约上做文章。
很显然，我也可以轻而易举做出对智能合约进行某种“验证”或者“静态分析”的工具，然而我深刻的知道，数理逻辑对于程序正确性的局限。很多程序是没法证明为正确，但它们确实是正确的。做这样的工作也许能圈到钱，然而却是非常枯燥而没有成就感的。为此，我拒绝了好几个区块链圈子里的合作，因为他们想利用我这方面的才能。我对智能合约的正确性验证不感兴趣，虽然我对区块链的其它一些部分是感兴趣的 ;)
如何保证智能合约的正确呢？你只有懂得如何写出正确的代码，非常小心。另外，静态分析和测试也可以有一些帮助，但要记住它们其实没法证明程序的正确。对于这个问题，你可以参考我的这篇文章。