今天我想来谈谈一个相关的话题：
以太坊式的智能合约的形式验证。有些人声称要实现基于“深度学习”的，自动的智能合约形式验证（formal verification），用于确保合约的正确性。然而今天我要告诉你的是，跟自动编程一样，完全自动的合约验证，也是不可能实现的。
随着
区块链技术的愈演愈烈，很多人开始在以太坊（Ethereum）的“智能合约语言”上做文章。其中一部分是搞 PL 的人，他们试图对 Solidity 之类语言写的智能合约进行形式验证，号称要用严密的数理逻辑方法，自动的验证智能合约的正确性。其中一种方法是用“深度学习”，经过训练之后，自动生成 Hoare Logic 的“前条件”和“后条件”。
版权申明：本内容来自于互联网，属第三方汇集推荐平台。本文的版权归原作者所有，文章言论不代表链门户的观点，链门户不承担任何法律责任。如有侵权请联系QQ：3341927519进行反馈。
