在之前一篇关于人工智能的文章中，我指出了自动编程的不可能性。 今天我想谈谈一个相关的话题：以太坊式智能合约的形式化验证。 一些人声称对智能合约进行基于深度学习的自动化形式验证，以确保合约的正确性。 但是，我今天要告诉大家的是，就像自动编程一样，全自动合同验证是不可能的。
随着区块链技术的深入，许多人开始对以太坊的智能合约语言大惊小怪。 他们中的一些人是从事PL的人，他们试图正式验证用Solidity等语言编写的智能合约，声称使用严谨的数理逻辑方法来自动验证智能合约的正确性。 一种方法是使用深度学习，深度学习经过训练可以自动生成 Hoare Logic 的前置和后置条件。
我好像把你弄糊涂了......让我们从 Hoare Logic 开始。
Hoare Logic 是一种形式验证方法，用于验证程序的正确性。 这样做的方法是先标记一些前置条件和后置条件（前置条件和后置条件），然后进行逻辑推理来验证**的一些基本属性，例如转移后的余额是否正确。 下面是一个非常简单的 Hoare Logic 示例：
这意味着，如果起始 x 等于 0，则在执行 x：=x+1 后，x 应大于 0。 前置条件为 x=0，后置条件为 x > 0。 如果 x 以零开头，则执行x:=x+1之后，x 将大于 0，因此将验证此句子。
Hoare Logic的系统将所有这些前置和后置条件与**连接起来，经过逻辑推导和验证，可以做出这样的保证：在前置条件满足的情况下，在**执行后，后置条件必须为真。 如果满足所有这些条件，系统将认为这是正确的过程。 需要注意的是，这里所说的“正确”完全是由人决定的，系统并不知道“正确”是什么意思。
Hoare Logic确实对程序的安全性有一定的影响，并且已经应用到一些实际项目中。 例如，在 Microsoft Windows 的驱动程序中，有一种称为 SAL 的安全注释语言，它实际上是 Hoare Logic 的实现。 但是，前置条件和后置条件是什么，你必须自己标记**，否则系统将无法工作。
例如，在上面的示例中，系统如何知道我想要 x>0 属性？只有我自己写的。 因此，要使用 Hoare Logic，您必须在 **. 如何编写这些条件需要对编程语言和形式逻辑的原理有深刻的理解。 这项工作需要训练有素的专家，并且需要大量时间。
因此，即使使用Hoare Logic，程序验证也不是一件容易的事。 于是，有人趁火抢，提出了一个与第一种药物类似的想法，声称他们会用深度学习来学习已经标注的**，最后让机器自动标注这些前后条件。 还处于幻想阶段，但已经写进了自动标注的优点中，作为自己的***我们的方法是自动的，其他项目都是手动的......
不幸的是，自动注释和自动编程一样是一种幻想。 自动编程的困难在于机器不知道你想做什么。 同理，自动标注的难点在于机器无法知道你想满足什么样的属性。 这些信息只存在于你的心中。 如果你不表达它，其他人或机器都不会知道它。
除非你把它写出来，否则机器永远不会知道函数的参数应该满足什么条件（前置条件），也永远不会知道函数的返回值应该满足什么条件（后置条件）。 例如，在上面的例子中，机器如何知道你在程序执行后希望 x 大于零？除非你告诉它，否则不可能知道。
你可能会问，深度学习不是吗？想想吧。。。。。。您可以为深度学习系统提供数千万条已经标记的行。 你可以标记整个Windows系统、整个Linux系统、Firefox，再加上一些战斗机、飞船，输入到深度学习系统中进行学习。 现在请问系统，**要写一个新函数，你知道我想做什么吗？你知道我希望它满足什么性质吗？你还不知道！只有我知道：这是:p曾经为我的猫铲屎
因此，使用深度学习来自动标注Hoare Logic前后的条件，就像自动编程一样，是在试图实现读心术，这显然是不可能的。 作为资深的PL和形式验证专家，这些人应该知道这不可能自动实现。 他们提出了这样的想法，并利用它作为优于其他智能合约项目的优势，当然，只是为了愚弄外行，为了发行货币;)
如果真的有可能使用深度学习来生成前置和后置条件，以完全自动地验证程序的正确性，那么这种方法应该在形式验证领域早就爆炸了。每个形式验证专家都希望能够完全自动地证明程序的正确性，但他们已经知道这是不可能的。
设计一种语言来告诉机器我们想要什么，什么是正确的，这本身就是PL专家和形式验证专家的工作。 一旦语言设计好了，我们就要依靠优秀的程序员来编写这些**，并告诉机器我们想做什么。 我们要依靠优秀的安全专家来标记前后的情况，并告诉机器什么叫正确和安全**，这一切都必须手动完成，不能由机器自动完成。
当然，我也不排除用 hoare 逻辑手动标记智能合约的可能性，这是有一定价值的。 我只想提醒大家，这些标签必须手动编写，不能自动生成。 此外，虽然该工具可以起到一定的辅助作用，但如果编写**的人不小心，则无法保证程序完全正确。
如何保证智能合约的正确性？这与确保程序的正确性是同一个问题。 只有懂得写得干净简单，思维严谨，才能写出正确的智能合约。 有关如何编写干净、简单和可靠的更多信息，您可以参考我以前的一些文章。
做智能合约验证的工作可能会赚钱，但很无聊，很不充实。 出于这个原因，我拒绝了几个与区块链相关的合作项目。 虽然我对区块链的其他一些想法很感兴趣，比如去中心化的共识机制，但我对智能合约正确性的验证一点也不乐观。
事实上，我认为智能合约的整个概念是不可靠的，是一个很大的误解。 在比特币和以太坊的系统中，根本不应该有脚本语言，也不需要脚本语言。
比特币的解锁脚本在开始时执行时出现低级错误，导致注入安全漏洞。 用户可能会恶意写入**，从而导致运行脚本的系统出现错误。 比特币最初的解锁方法是将**（解锁脚本+锁定脚本）的两段拼接成文本，然后执行。 程序的文本处理是编程语言实现的禁忌。 有一点经验的黑客知道这里可能会有攻击点。
以太坊的 Solidity 语言始于一个低级错误，导致价值 5000 万美元的以太币被盗。 以太坊的智能合约系统消耗了大量的计算资源，也导致了严重的性能问题。
虽然比特币和以太坊的作者可能是密码学和分布式系统领域的专家，但我不得不承认，他们都是PL的外行:p但是，如果您是这些语言的专家，那不是更好吗？我不这么认为。
第一个问题是PL领域充满了各种宗教，传教士也很多。 普通的 PL 内部人员会通过试图设计一种完美的语言来表达自己的信仰，而不管他人的生活如何，从而使事情复杂化。 如果你运气不好，你会遇到那种极客......充满纯函数、单子、依赖类型、线性逻辑然后语言被设计成没有人可以使用:p
负责任的PL科学家，他们都试图避免首先创造新的语言。 如果可以在没有新语言的情况下解决问题，就不要设计新语言，尽量不要在系统中使用嵌入式语言。 所以，如果我设计了比特币，我根本不会为它设计一种语言。
让用户可编程是很危险的！很少有用户能够正确可靠地编写**，并且很少有语言系统能够开发出没有错误。 语言系统设计中的错误可能会给黑客编写恶意脚本进行破坏的机会。 从来没有任何语言和它们的编译器，运行时系统从一开始就是正确的，需要很多年才能稳定下来。 然后你必须考虑性能，这对于去中心化的分布式系统来说更加困难。 对于普通语言来说，这不是什么大问题，你不需要用它来控制飞机。 然而，数字货币系统的语言几乎不允许这个问题。
因此，与其担心设计这些智能合约语言，不如完全不要使用这种功能。
我们真的需要这些脚本的功能吗？虽然比特币有脚本语言，但实际上常用的脚本不超过 5 个，你可以直接硬编码它。 虽然以太坊的***已经做了这么多的应用前景，但EVM上有什么有价值的应用吗？我认为我们不需要这些智能合约。 只要数字货币做好一件事，就可以安全高效地当钱使用，这已经很好了。
美元、人民币、**他们有合约功能吗？不。 为什么数字货币必须具有这样的功能？我觉得这违反了模块化设计的原则：一件事只做一件事，而且做得最好。 数字货币应该像货币一样，可以实现转账兑换的简单功能。 合约应该是一个单独的系统，不应与货币相关联。
合同呢？将其留给律师和会计师，或使用单独的系统。 你有没有想过为什么世界上的法律体系没有被编程为自动化？为什么我们需要律师和法官，而不仅仅是机器人？为什么一些国家法院有必要有陪审团，而不仅仅是根据法律条款来裁决案件？这不仅仅是一个历史问题。 你需要了解法律的本质，才能明白在没有人类的情况下机械地执行法律是不可行的。 智能合约就是要把人们完全带出系统，这将是一个问题。
期望过多的功能实际上是过度设计。 花费精力折腾智能合约系统可能会大大延迟世界对数字货币的真正接受。 说实话，在尝试了多种数字货币，了解了它们使用的技术后，我发现它们挺有意思的，但这些数字货币还处于实验阶段，离真正被当成货币使用还有一定的距离。 专注于改善它们作为货币的功能将加速它们的接受。 把精力花在智能合约上，我认为这是一个错误。
在这一点上，我认为比特币比它的继任者（例如以太坊）更真实一些。 比特币也有一种脚本语言，但它并没有过分强调这种脚本的作用。 比特币的脚本语言非常简单，而且不是图灵完备的。 这迫使用户编写功能简单、不会损害系统性能且易于验证的脚本。 相比之下，以太坊花费了太多精力来折腾智能合约，使它们过于复杂，导致各种问题并影响对最重要的货币特征的接受。