> One concern with logic programming is cost of computation, Right, but the client executes the contract, keeping a trace of what needs to be computed by the v

> One concern with logic programming is cost of computation, Right, but the client executes the contract, keeping a trace of what needs to be computed by the verifier. The verifier doesn't actually execute the full contract, just verifies that the trace was faithfully executed. If we have let R = (A() || B() || C() || D()) && ! E(); R(). If A is costly, but true 99% of the time, but this transaction is one of the 0.001% of the cases where D() is true, the contract verification trace says to execute D(), and the verifier never checks A, B, or C. See my nearby comment for a worked out example of a compact trace representation for a deeper disjunction decision tree. Effectively, because declarative languages don't dictate order, the client is free to re-order the contract execution order to be optimal for this particular execution, without altering semantics. Declarative semantics, are by definition, independent of execution order. This makes efficient compilation and execution more difficult, but makes verification faster (if the verifier is provided with an execution trace). Now, you could potentially do similar optimizations with Solidity contracts, with a suitably modified EVM definition, but if the execution order is up to the runtime/compiler instead of dictated by the source code, then you've by definition changed the language to be declarative.