Public, permissionless blockchains promise to enable financial contracts between anonymous agents which are enforced programmatically, enabling a new form of disintermediated, economic collaboration between participants. Such agreements are called “Smart Contracts”, a term first coined by Nick Szabo [1].
The history of transactions in a blockchain is immutable [2], which provides strong security guarantees for the execution of Smart Contracts. However, this also sets very high standards on the specification and implementation of such contracts, since these can programmatically manage large amounts of funds and cannot be arbitrarily updated after deployed on the blockchain. As a consequence, exploits of underspecified smart contracts remain a common challenge.
This project aims to research Smart Contract languages with formal safety guarantees. Financial smart contracts implemented in general-purpose contracting languages are generally very complex and difficult to formally verify. Instead, we are interested in domain-specific smart contract language approaches, which focus on specific application domains, such as decentralised finance. Furthermore, this project investigates how smart contracting language development can facilitate blockchain scaling and privacy.
Ultimately, we aim to contribute knowledge and technology to facilitate the development of formally secure, smart contracts, so that users and engineers can efficiently and safely build the decentralised, permissionless applications of tomorrow.
[1] Szabo, Nick. “Smart Contracts: Building Blocks for Digital Markets”, 1996.
[2] Nakamoto, Satoshi. “Bitcoin: A peer-to-peer electronic cash system”, 2008.