Cryptocontracts Will Turn Contract Law Into a Programming Language

How does the automatic enforcement work? Specifically, how would the software algorithmically determine whether one party has performed satisfactorily?

Determining whether one party has paid the other is relatively straightforward--compared to other contractual obligations, at least. Whether it relies on a centralized model like a bank, or something decentralized like BitCoin, it's easy to quantify and measure the exchange of money.

What's harder is measuring the other side of the contract. How does the software know that the plumber has satisfactorily installed the customer's new shower? Or that the web developer has built a satisfactory website for the client? Or that the mortgager has encumbered his home in violation of the mortgage?

Also: when program hits a missing case in a switch statement, throwing an exception and rebooting the program is an option. That's not true for the equivalent situation with contracting parties.

>high-frequency trading in Python

Wait...they're willing to spend millions to build a new undersea cable that shaves a millisecond off the latency...but they use an interpreted language? How does that work?

I'm sorry for the grammatical ambiguity. The regulations themselves were to be written in Python. Nonetheless, I do think interpreted languages are used in HFT, but presumably not the kind of HFT that attempts to exploit inefficiencies between in, say, the prices of frozen concentrated orange juice futures on the Chicago Mercantile Exchange vs the price of agricultural companies on the New York Stock Exchange.

I think this is interesting debate, so without detracting from the importance of these questions here are some answers of mine:

1. I don't think this is a linguistic restriction as much as a denotation of the scope of a contract formal language. Real world actions like this could perhaps be recorded by a neutral third party (accepted via cryptographic signature with the necessary identity components baked into the script of the contract itself). I think more broadly that the scope of this formal language would be less around verification and enforcement and more around producing automated analysis of the content of a contract.

2. Continuing from point (1), this is exactly what I see the point of a contract formal language is—by becoming exhaustive about what kinds of things can be described in a contract we can check exhaustively (automatically) whether or not a contract is well-formed. You might be able to ask questions like "given I've defined these 18 eventualities, are all of them eventually observed and handled properly?". These kinds of questions are related to typing, termination[1], and totality checks, all of which are done in programming languages.

([1] Note, termination can be checked for a subset of all programs without violating the Halting Problem—you just won't have a Turing Complete contract language, which doesn't seem particularly problematic.)

3. This is definitely an interesting point—I'd imagine that large, complex, fully-automated, and self-executing cryptocontracts are much, much further off than cryptocontracts used in combination with a court. If a court is an exception system then a nice contract formal language just makes it easier to go further without depending as much upon exceptions---but they're still there for when the shit really hits the fan.

4. I think this is certainly true—for the last 40 years of building programming languages it's clear we're pretty inundated with shitty ones. But that said, for as painful as reusability is sometimes, we do get a lot of reusability. It might be unbelievably challenging to write the first lease cryptocontract, but if it was done well then the components which built it could be recycled, re-parameterized, and re-combined into other similar contracts with ease. The constraints of a contract formal language could ensure that these recombinations are sensible and other program analyses can ensure that it's, say, enforceable and complete.

I think it definitely transitions the challenges from interpretation and maintenance of contracts toward front-loaded concerns like contract composition and extensibility, but once that's done we have much firmer grasp on contract reusability. That's clearly a valuable thing given how often contracts are just mid-libbed between parties already—a contract formal language could make it easier, saner to reuse old contracts.

---

So, I'd definitely come off saying that a contract "programming language" is probably not going to look as much like a programming language that most programmers today are familiar with and more like a formal language such as mathematics or Coq where power is sacrificed for analyzability. As always with programs, the real-world interface is one of the most painful, but that's often what cryptographic technology provides---ways of translating messy real world actions into limited, binary, unforgeable digital effects (the 1-0 effect of having a cryptographic key versus the messy effect of being at fault).

From what I've seen of the Bitcoin protocol it's going to be useful for things like escrow, but is a far, far, far cry away from a meaningful place to specify more interesting contracts.