5 ms·
This doesn't sound right to me. Contract law should not require turing completeness. First order logic should be more than sufficient. How does having a loop in
by dkarapetyan 10y ago
This doesn't sound right to me. Contract law should not require turing completeness. First order logic should be more than sufficient. How does having a loop in contract law make any sense?
- conception 10y agoWould regular payments based on criteria be an example? A paycheck basically.
- naasking 10y agoThis argues for a temporal logic, not for recursion. Something like: http://szabo.best.vwh.net/contractlanguage.html http://szabo.best.vwh.net/contractlanguage.html
- wyager 10y agoThere are also a class of total languages (Coq, Agda, Idris) that are guaranteed to terminate but admit (polymorphic) recursion. This is stronger than FOL but weaker than turing-completeness, and certainly sufficient to implement any feasible contract.
- dkarapetyan 10y agoI agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.
- wyager 10y ago> in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.
- dkarapetyan 10y agoI don't think accessibility is a bad thing. I think computing, its practice and theory, should be taught the same way we teach literacy. I didn't mean "average" as in "incompetent". If writing contracts was as simple as writing a few lines of code in some formal language that didn't require a law or finance degree then I would consider that to be a good thing. It would be even better if the system was designed from first principles with solid theory backing it.
- wyager 10y agoI totally agree, but the reality is that in order to write contracts that are sure to be correct, you need a level of expertise that involves much more work than just learning how to write programs. Knowing the syntax and usage of a rigorously-typed language like Agda is the easy part.
- kowdermeister 10y agoThen the platform is flawed. Average programmers should be able to understand it easily. It's not that hard, some wants X and some wants Y in exchange. I'm not a lawyer but I write contracts with my clients. If you keep things simple it should fit most people. making g smart contracts complicated you keep it in the area of a small elite who are knowledgeable of playing safe with it. I wold go as far as make it as simple as HTML.
- wyager 10y agoThat's what standardized contracts are for. Tellers don't write the legalese on your credit card receipt. They just print it out.
- Paradigma11 10y agoBut : https://en.wikipedia.org/wiki/Solidity https://en.wikipedia.org/wiki/Solidity "As specified by Wood it is designed around the ECMAScript syntax to make it familiar for existing web developers;"
- plaguuuuuu 10y agoI agree. Furthermore, the notion of contracts that cannot be specified in first-order logic seems relatively dangerous to me.
- mbrock 10y agoCould you expand on how one would specify DAO-like contracts with only first-order logic?