A Language Stack for Implementing Contracts

The term Smart Contract is used for arbitrary programs that run on the distributed, trustworthy computing infrastructure provided by a blockchain. However, the sweet spot for such programs is actual contracts, i.e., long-running, collaborative processes involving several parties who may or may not trust each other. To implement such contracts effectively, we need much more than the Blockchain: contracts must be expressed in a way so that the relevant stakeholders, who are not typically programmers, can understand the them; contracts must be functionally correct, i.e., they must behave in exactly the way the stakeholders expect; and they must be protected against being gamed, for example, through sybil attacks. The trust in the execution of the contract, mostly through non-repudiability, is then provided by the blockchain. In this talk, I discuss research into how to formally model contracts, I present languages that are suitable for representing contracts in a way that is lawyer-accessible and prevents some aspects of gaming, and I discuss how such approaches lead to improved correctness through correctness-by-construction and simplified verification.