I see that Pact can automatically check certain properties of smart contracts using Microsoft's Z3 theorem prover. Are there relevant properties of smart contracts that can't be verified automatically? If there are, do you expect to verify them on a case-by-case basis, or is there work being done to expand the capabilities of the automatic checker?
Also, do you expect Pact's Turing incompleteness to limit smart contract developers in any meaningful way?
For the first question: A huge benefit of Pact having a disciplined runtime environment and structure is the potential to admit the whole language to the FV environment. Pact 3.0 (the next version which will release with Chainweb Testnet) gets most of the way there, including coverage for “pacts”, our multi-step abstraction. Note, however, that this can result in all sorts of actions being unverifiable -- but that’s a feature, not a bug. If you want correct code you have to walk a narrow path.
Re: Turing Incompleteness, only in that certain tools are off-limits, namely recursion, but also anonymous lambdas (which would allow introduction of y-combinators). The latter is less onerous as its main impact is on expressiveness which honestly contradicts our policy of “easy to understand code”: expressive code while powerful is often experts-only. Plus, Pact has advanced functional features like partial application (used in map and fold for instance) that languages like Solidity (and frankly, Javascript) lack. Recursion is a more significant drawback but here we’re opinionated: a blockchain is a cost-regulated environment and recursion where it is really needed (note that Pact can do bounded looping via the above-mentioned structures) indicates a use-case that is ill-suited for a shared-compute environment, such as pathfinding etc. So, an advanced Pact dev might have to unroll some algorithm into a bounded loop but that’s a reasonable price to pay for the huge increase in safety.
