Correctness proofs of distributed systems with Isabelle/HOL
Channel: Martin Kleppmann
Date: 2019-12-11

This is an extended version of a talk given at Strange Loop 2019 and Code Mesh London 2019.
Isabelle code: https://gist.github.com/ept/b6872fc541a68a321a26198b53b3896b
Slides & more info: https://martin.kleppmann.com/2019/09/14/strange-loop-isabelle.html

Abstract:
Testing systems is great, but tests can only explore a finite set of inputs and behaviours. Many real systems, especially distributed systems, have a potentially infinite state space. If you want to be sure that a program does the right thing in all possible situations, testing is not sufficient: you need proof. Only mathematical proof, e.g. by induction, can cover an infinite state space.

Pen-and-paper proofs are well established in mathematics, but they need to be laboriously checked by hand, and humans sometimes make mistakes. Automated theorem provers and computerised proof assistants can help here. This talk introduces Isabelle/HOL, an interactive proof assistant that can be used to formally prove the correctness of algorithms. It is somewhat like a programming language and interactive console for proofs.

In this talk we will explore how Isabelle can be used to analyse algorithms for distributed systems, and prove them correct. We will work through some example problems in live demos, and prove real theorems about some simple algorithms. Proof assistants still have a pretty steep learning curve, and this talk won’t be able to teach you everything, but you will get a sense of the style of reasoning, and maybe you will be tempted to try it for yourself.