I'm not convinced there's great utility in smart contracts, but if there is, I think there's a huge utility in contracts being declarative and statically typed, to avoid many of the problems we've seen with existing contracts. In that case, a statically typed Prolog dialect would be a good starting point. The contract would be a set of declarative rules describing acceptable next states of the contract. To make the contracts verifiable in linear time, the submitter would submit the next state of the contract, plus a compact binary representation of the path taken through the rules set, so no backtracking would occur in the verifier. You could allow recursion, as verification time would still be linear in the size of the submitted compact path representation, just not linear in the size of the contract. If you disallow recursion, then verification would also be linear in the size of the contract.
Granted, many of the problems with Ethereum Solidity contracts are more to do with all of its use of implicit behavior (in a misguided attempt to hide the complexity of contracts) rather than directly consequences of Solidity being imperative.
Here's a quick plug for Mercury[0], a statically typed dialect of Prolog with an optimizing native code compiler. Supposedly it's 5 to 10 times faster than commercial Prolog compilers or available interpreters.
Lira[0] and its readable paper[1] is a good example of abstracting smart contracts into a statically typed, domain-specific language that describes the contract precisely at a high level. It's not Turing complete, which works for a large class of contracts (for instance, see the American and Asian options examples in [1]).
One concern with logic programming is cost of computation, on Ethereum every transaction has a gas associated with it and so you can't run computations that go over the gas available in a block.
Turner's ideas of Total Functional Programming[2] might have application in the smart contract space as well, since you disallow general recursion but allow structural recursion, you can likely precalculate or bound gas costs accurately ahead of time.
As for being statically typed, I completely agree, Solidity's poor design choices contributed to millions of USD in loss (e.g. DAO hack) because the developers were not able to easily reason about the implicit behavior or concurrency model.
> 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.
> DAO hack) because the developers were not able to easily reason about the implicit behavior or concurrency model.
I believe the DAO bug was a reentrancy bug, not a concurrency bug. The code was not written to be reentrant because the developer didn't realize recursion could be triggered via implicit behavior. Many reentrancy bugs are concurrency bugs, but I really think that's not the case with the DAO bug. I saw one proposed fix (not sure if it's the one that got finally accepted) that used a reentrancy flag to prevent the problem and called the flag a "mutex", but it wasn't actually a mutex, adding to the confusion about the root cause.
I really don't think execution of a single contract transaction is concurrent, and due to (eventual) serializability of blockchain transactions, the blockchain acts as if concurrent execution within a contract across miners doesn't exist. If you have concurrent calls to a single contract, at most one of them will succeed, and those that fail will not affect the blockchain state.
In general, the Ethereum community seems to refer to serialized execution of contract methods in an order unexpected by the contract author as "concurrency", but I have seen no evidence that the effects on the contract state as reflected in the blockchain are not always serializable. In other words, it acts much like concurrent SQL queries under a serializable isolation level: if two concurrent executions modify the same data, one of them will fail instead of you getting an interleaving of the two write sequences.
It's possible that I misunderstand the EVM, but it seems insane to design a system to allow multiple threads to execute within a single contract at a time in the presence of shared mutable state, at least without an RDBMS-like isolation system in place.
You should check out the Digital Asset Modeling Language, DAML. [0]
They've built a language for distributed ledger platforms based on Haskell with defined state transitions based loosely on traditional contract law. For exactly the reasons you've mentioned, this makes modeling the participants, rights, and obligations of a smart contract use case incredibly efficient.
Whether smart contracts are useful or not remains to be seen. There seems to be a lot of potential in the finance and supply chain worlds.
When thinking about DAML it makes me wonder how impactful something like Cobol was in reality. Definitely found use and even long term value add, but transformational? I don't know.
I'm not even sure what the technology comparison should be for DLT without DAML. There's only so many use cases or niche areas where it's valuable.
I presume DAML is based loosely on SPJ's "Composing Contracts" paper. A few years ago at work, I was involved with a compiler from a DSL loosely based on SPJ's Composing Contracts. The compiler is a transpiler from contract descriptions to Cuda/OpenCL/ISPC code that runs a Monte Carlo simulation to calculate theoretical present value of the contract. The use case is complex derivative pricing and risk management.
Interesting point. The biggest counter-argument I see is the need for fine-grained optimization of gas usage. Especially given the crazy high fees as of late.
Hand-tuned imperative C enjoys a performance advantage over functional and declarative alternatives. So I’d imagine that imperative smart contracts are inherently easier to optimize than Prolog-style contracts.
While I prefer declarative languages, it is also interesting to note very simple imperative languages are often the easiest to verify formally (as transition systems).
The thing is that declarative contracts separate execution from verification. You don't actually execute the contract in the miner/verifier. The client executes the contract and records a trace of the subset of the program necessary to verify execution. The miner/verifier just uses the trace to verify that the presented state is correct (top-level contract rule evaluates to true).
In the simple and common cases, there ends up being no difference between execution and verification. However, if you have a contract that has
let F = (A() || B() || C() || D()) && ! E();
let R = F() && (G() || H());
R();
with an imperative contract that gets executed on the verifier, you need to optimally order the clauses A-D, taking into account the cost of each and the percentage of the transactions in which each one is true. The client isn't allowed to re-order the clauses in the contract. With a declarative contract that is executed client-side, the client tells the verifier exactly which one of the terms A-D needs to be evaluated and which of the terms G-H needs to be evaluated. Let's say G and D are the lowest cost functions that need to be evaluated to verify our transaction. If the execution trace is the child index taken in depth-first traversal of the tree of logical disjunctions in the contract expression then the trace indicating that D and G need to be evaluated is [3, 0]. This can be compactly represented as a single (potentially large) integer in a mixed-base number system. (In our case, the bases are 4 and then 2, so the single integer representing the trace is 2*0 + 3 = 3. The verifier first hits a 4-way disjunction, and 3 mod 4 is 3, so it only evaluates the 4th branch. 3 div 4 is 0. It next hits a 2-way disjunction and 0 mod 2 is 0, so it only evaluates the 1st branch.) If you order the logical disjunctions in your contract so that in the common case, the leftmost alternative is always taken, then in the common case, your execution trace as a mixed base integer is 0. With estimates of the probabilities of the branches, you could use an asymmetric mixed base number system, similar to Facebook's zstd compression to optimally represent your verification traces.
With a declarative contract, the cost of suboptimal ordering is borne by the client and not by the verifier.
With EVM, there's no separation of contract execution and verification. The verifier/miner needs to execute the contract at the request of the client. If you modify the EVM and contracts to keep track of what's provably side-effect free and allow the client to specify reordering of those terms, then you've by definition created a non-imperative language or sublanguage. In that case, it's much safer and easier to design the system from the ground up to have semantics that are invariant under evaluation order (that is, declarative semantics).
Most of the cost of declarative program optimization vs. imperative program optimization (deciding an optimal order) is borne on the client side. Due to the structure of the contracts and the traces, it's trivial to prove that portions of the contract don't need to be executed in order to verify the transaction.
I'm familiar with factor. The thing about factor is that its execution semantics depend on execution order (i.e. imperative), which makes it impractical / unsafe to allow clients to provide verifiers with an optimal execution order for verifying a contract.
Granted, many of the problems with Ethereum Solidity contracts are more to do with all of its use of implicit behavior (in a misguided attempt to hide the complexity of contracts) rather than directly consequences of Solidity being imperative.
Here's a quick plug for Mercury[0], a statically typed dialect of Prolog with an optimizing native code compiler. Supposedly it's 5 to 10 times faster than commercial Prolog compilers or available interpreters.
[0] https://github.com/Mercury-Language/mercury