A Language Stack for Implementing Contracts
This video is also available in the GOTO Play video app! Download it to enjoy offline access to our conference videos while on the move.
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.