pact-lang - Pact 形式验证属性

Question

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

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

Answer 1

对于第一个问题:具有规范的运行时环境和结构的 Pact 的一个巨大好处是有可能将整个语言纳入 FV 环境。 Pact 3.0(下一个版本将与 Chainweb 测试网一起发布)完成了大部分工作，包括对“pacts”的覆盖，我们的多步骤抽象。但是请注意，这可能会导致各种操作无法验证——但这是一个功能，而不是错误。如果你想要正确的代码，你必须走一条狭窄的道路。

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