契约正式验证属性

Question

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

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

Answer 1

对于第一个问题：具有规范的运行时环境和结构的Pact的巨大好处是将整个语言纳入FV环境的潜力。Pact 3.0（将与Chainweb Testnet一起发布的下一个版本）可以实现大多数方式，包括对“步骤”（我们的多步骤抽象）的介绍。但是请注意，这可能导致各种动作无法验证-但这是功能，而不是错误。如果您想要正确的代码，则必须走很窄的路。

回复：图灵不完整，仅在某些工具是禁止使用的，即递归，还有匿名lambda（允许引入y组合器）。后者不那么繁重，因为它的主要影响是对表达性的影响，这与我们的“易于理解的代码”政策相抵触：表达性代码虽然功能强大，但通常仅是专家。另外，契约具有先进功能的功能，如局部应用程序（在使用map和fold例如）缺少Solidity（坦率地说是Javascript）之类的语言。递归是一个更严重的缺点，但在这里我们认为：区块链是一种成本受控的环境，在真正需要递归的地方（请注意，Pact可以通过上述结构进行有界循环）表明一个用例是因此，高级Pact开发人员可能不得不将某些算法展开到有界循环中，但这是为安全性的巨大提高付出的合理价格。