7 ms·

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,

by KMag 6y ago

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. [0] https://github.com/Mercury-Language/mercury https://github.com/Mercury-Language/mercury

dfischer 6y ago
Similarly down this path I found Factor. A different approach but supports backtracking. https://factorcode.org/ https://factorcode.org/
- KMag 6y ago
  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.
dcolkitt 6y ago
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.
- KMag 6y ago
  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.
siraben 6y ago
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. [0] https://github.com/etoroxlabs/lira https://github.com/etoroxlabs/lira [1] https://bahr.io/pubs/files/bahr15icfp-paper.pdf https://bahr.io/pubs/files/bahr15icfp-paper.pdf [2] http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf http://www.jucs.org/jucs_10_7/total_functional_programming/j...
- KMag 6y ago
  > 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.
TheColorYellow 6y ago
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.
- KMag 6y ago
  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.

by KMag 6y ago

dfischer 6y ago

Similarly down this path I found Factor. A different approach but supports backtracking. https://factorcode.org/ https://factorcode.org/

KMag 6y ago
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.

dcolkitt 6y ago

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.

KMag 6y ago
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.

siraben 6y ago

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. [0] https://github.com/etoroxlabs/lira https://github.com/etoroxlabs/lira [1] https://bahr.io/pubs/files/bahr15icfp-paper.pdf https://bahr.io/pubs/files/bahr15icfp-paper.pdf [2] http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf http://www.jucs.org/jucs_10_7/total_functional_programming/j...

KMag 6y ago
> 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.

TheColorYellow 6y ago

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.

KMag 6y ago
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.