4 ms·

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

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.
KMag 6y ago
> 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. Edit: https://forum.ethereum.org/discussion/1317/reentrant-contracts https://forum.ethereum.org/discussion/1317/reentrant-contrac... supports my understanding.

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.

KMag 6y ago

> 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. Edit: https://forum.ethereum.org/discussion/1317/reentrant-contracts https://forum.ethereum.org/discussion/1317/reentrant-contrac... supports my understanding.