I'm wondering if there has been any work done on the decidability of real world, legal contracts.

Michelson is great because it lends itself to users bring able to write smart contracts that are provably correct (in terms of termination and resource usage).

I wonder if the same can be said for legal contracts out there in the real world?

1 Answer 1


Smart contract executions are limited by finite limit on the length, and finite limit on the gas. That means that their properties are decidable for a given version of the protocol.

Many real-world legal contracts and regulations have been often expressed as simple Prolog programs without loop. These would be decidable as long as material conditions of the contract are decidable. It can be argued that most of real-world contracts fall into this class.

Good example would be a rental contract, where material conditions are occupation of the room by a renting party, and making it available by the room owner. This type of contact is decidable.

But it is perfectly reasonable to sign a contract on the implementation of a program specification. If the program specification is complex enough, it will likely contain some Turing-complete scripting language, thus possibly rendering a complete fulfillment of this legal contract undecidable.

In practice courts would then decide on good faith effort to implement it, or award a partial payment, but that is just a workaround in legal systems where actors do not have infinite time to decide cases.

But in generality just legal contracts on software delivery are already undecidable.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.