Just Testing

This is the video of the keynote talk “Blockchains are functional” that I delivered at the ACM SIGPLAN International Conference on Functional Programming 2019. Here is the abstract:

Functional programming and blockchains are a match made in heaven! The immutable and reproducible nature of distributed ledgers is mirrored in the semantic foundation of functional programming. Moreover, the concurrent and distributed operation calls for a programming model that carefully controls shared mutable state and side effects. Finally, the high financial stakes often associated with blockchains suggest the need for high assurance software and formal methods.

Nevertheless, most existing blockchains favour an object-oriented, imperative approach in both their implementation as well as in the contract programming layer that provides user-defined custom functionality on top of the basic ledger. On the one hand, this might appear surprising, given that it is widely understood that this style of programming is particularly risky in concurrent and distributed systems. On the other hand, blockchains are still in their infancy and little research has been conducted into associated programming language technology.

In this talk, I explain the connection between blockchains and functional programming as well as highlight several areas where functional programming, type systems, and formal methods have the potential to advance the state of the art. Overall, I argue that blockchains are not just a well-suited application area for functional programming techniques, but that they also provide fertile ground for future research. I illustrate this with evidence from the research-driven development of the Cardano blockchain and its contract programming platform, Plutus. Cardano and Plutus are implemented in Haskell and Rust, and the development process includes semi-formal specifications together with the use of Agda, Coq, and Isabelle to formalise key components.

Extending Bitcoin-style Ledgers

In the Plutus & Marlowe team at IOHK, we developed an extension to Bitcoin-style UTxO ledgers that we are calling the Extended UTxO Model and that significantly extends the contract scripting capabilities of such ledgers. On top of that new, more powerful ledger model, we developed a domain-specific language for financial contracts, called Marlowe. We have got two papers at the 4th Workshop on Trusted Smart Contracts where we describe both the Extended UTxO Model and Marlowe. Check out the preprints: The Extended UTxO Model and Marlowe: implementing and analysing financial contracts on blockchain.

Functional Blockchain Contracts

Check out the draft of the paper describing the principles underlying Plutus Platform. Here the abstract:

Distributed cryptographic ledgers —aka blockchains —should be a functional programmer’s dream. Their aim is immutability: once a block has been added to the chain it should not be altered or removed. The seminal blockchain, Bitcoin, uses a graph-based model that is purely functional in nature. But Bitcoin has limited support for smart contracts and distributed applications. The seminal smart-contract platform, Ethereum, uses an imperative and object-oriented model of accounts. Ethereum has been subject to numerous exploits, often linked to its use of shared mutable state by way of its imperative and object-oriented features in a concurrent and distributed system. Coding a distributed application for Ethereum requires two languages: Javascript to run off-chain, which submits transaction written in Solidity to run on-chain.

This paper describes Plutus Platform, a functional blockchain smart contract system for coding distributed applications on top of the Cardano blockchain. Most blockchain programming platforms depend on a custom language, such as Ethereum’s Solidity, but Plutus is provided as a set of libraries for Haskell. Both off-chain and on-chain code are written in Haskell: off-chain code using the Plutus library, and on-chain code in a subset of Haskell using Template Haskell. On-chain code is compiled to a tiny functional language called Plutus Core, which is System Fω with iso-recursive types and suitable primitives.

Plutus and Cardano are available open source, and Plutus Playground provides a web-based IDE that enables users to try out the system and to develop simple applications.

PLT engineers needed!

Do you know how to write FP compilers? Would you like to design & implement next-generation, functional(!) smart contract languages with Phil Wadler and myself? Check out Phil’s post and the IOHK job ad.