Pact形式验证属性

Question

我看到Pact可以使用微软的Z3定理证明器自动检查智能合约的某些属性。智能合约是否存在无法自动验证的相关属性？如果有，您是否希望逐个验证它们，或者正在进行扩展自动检查器功能的工作？

此外，您是否希望Pact的图灵不完备性会以任何有意义的方式限制智能合约开发人员？

Answer 1

对于第一个问题: Pact有一个有纪律的运行时环境和结构的巨大好处是有可能允许整个语言进入FV环境。Pact 3.0 (将与Chainweb Testnet一起发布的下一个版本)在那里获得了大部分内容，包括对“Pact”的覆盖，我们的多步骤抽象。但是，请注意，这可能会导致所有类型的操作都无法验证--但这是一个特性，而不是一个bug。如果你想要正确的代码，你必须走一条狭窄的小路。

Re:图灵的不完备性，只是因为某些工具是禁止的，即递归，还有匿名的lambda(这将允许引入y-组合器)。后者不那么繁琐，因为它的主要影响是对表达性的影响，这与我们的“易于理解的代码”的政策相矛盾:表达性代码虽然强大，但通常只有专家才能使用。此外，Pact还具有高级功能特性，如部分应用程序(例如，在map和fold中使用)，而Solidity (坦率地说，还有Javascript)等语言缺乏这些特性。递归是一个更大的缺点，但在这里我们坚持认为:区块链是一个成本控制的环境，在真正需要它的地方(请注意，Pact可以通过上面提到的结构进行有界循环)表示一个不适合共享计算环境的用例，例如寻径等。因此，高级Pact开发人员可能不得不将一些算法展开到有界循环中，但对于安全性的巨大提高来说，这是一个合理的代价。