proofcraft.org

So you want to be a proof engineer?

 

The easiest way to learn interactive theorem proving is to take a University course in that topic. There are many of these around, but not everyone can be that lucky. You can teach yourself interactive proof from books and by working through exercise projects. These exercise projects are more important than the reading. Don’t skip them.

Disclaimer:

• I know most of the authors of these books and am a co-author on one of them myself.
• The following assumes you’re after learning interactive proof and program verification in Isabelle/HOL.

Functional Programming

The first step to interactive theorem proving is functional programming. If you’re fluent in a language such as ML, OCaml, Haskell, or F# you’re in luck: you’re already halfway there, and may skip to step two. If not, you will learn something that will make you a better programmer even if you do not end up proving theorems or formally verifying software. I get more calls from recruiters looking for functional programmers than for any other kind of expertise in our research group.

Why is functional programming a prerequisite? Because the proof language of Isabelle/HOL is Higher-Order Logic (HOL), and HOL is functional programming + logic.

Functional programming will introduce you to thinking in terms of recursion instead of iteration and equations instead of operations. It will encourage you to express yourself in algebraic data types and pattern matching and to appreciate type variables and functions as values.

ML

So, which language to pick? If you are looking to learn Isabelle/HOL, the language ML is a good candidate. ML is short for Meta Language. You might say it was invented for writing theorem provers.

Isabelle is written in ML and Scala. Even though it is not necessary to know ML for writing proofs in Isabelle, Isabelle’s syntax for types and functions is close to standard ML, so things will look familiar. ML has been around for a while and while expressive and powerful, is one of the simpler functional languages to learn. It may also come in handy later down the track when you are looking at larger, more complex projects and at extending the prover yourself. In short, if you’re going to learn a functional language anyway, there are worse options to pick.

The book ML for the Working Programmer by Larry Paulson at the University of Cambridge is an excellent introduction to the language. One of the projects in the book is writing a little theorem prover, so you’ll feel right at home when you are graduating to Isabelle.

If you are impatient, you don’t need to deeply know everything ML has to offer before you can proceed to proofs. You can safely skip modules and functors for a while, but be sure to feel comfortable with recursion, patterns, higher-order functions, and polymorphic types.

Haskell

ML is not everybody’s first pick. For one, it has state, that is, mutable references like imperative languages do. They are in the language because it was believed they were necessary for efficiency. These days, at least in Isabelle, it turns out that it is better to eliminate mutable state wherever possible, because it makes it hard to exploit the concurrency multi-core machines have to offer.

If ML is not your cup of tea, and you are looking for something pure that is used in real-world industrial applications, learning Haskell is a good alternative. It is used extensively in the financial world, but also in high-assurance applications. It has a thriving user community and a large repository of libraries.

The syntax is close enough to Isabelle that it won’t throw you off too much, and the basics of types and recursion are the same.

There are almost too many tutorials for Haskell around. I happen to like the book Real World Haskell by Bryan O’Sullivan, Don Stewart, and John Goerzen. It starts with an accessible tutorial-style introduction to the language, but keeps things interesting later with issues that you will encounter if you are using the language for real projects.

I have also heard good things about the tutorial Learn You a Haskell for Great Good. It’s quirky and will do the job if you like the style.

When learning Haskell, be sure to check out the type class feature of the language. Isabelle has a similar albeit much simpler one.

Machine-Checked Proof

You know functional programming. Step two: theorem proving.

We have just the book for you: Concrete Semantics by Tobias Nipkow and myself. Before you start thinking this post is just after advertising and money: there is a free online version of the book available at http://concrete-semantics.org.

The book has two parts. The first part is an introduction to Isabelle, in particular to writing functional programs in Isabelle and how to prove properties about them. You learn classical Higher-Order Logic and things like proof by induction, you also learn how to use Isabelle’s automation and counter-example finder.

The second part is about the semantics of programming languages. The book shows how to define the meaning of programs in the theorem prover and the fundamentals of how to analyse the behaviour of programs and properties of whole languages. It works through a number of analyses and optimisations you can perform on programs, such as data flow analysis, abstract interpretation, or security type systems. It also teaches the fundamentals of Hoare-Logic, which is one of the main techniques for verifying programs.

If you are mainly interested in program verification, you will want to read the first part, and the second part up to Hoare-Logic. The rest is informative for program verification, but optional.

If you prefer a more condensed version of the material in the form of slides, there is also lecture material available for the book.

Concrete Semantics is not the end, but the beginning of learning program verification in Isabelle. However, after this book, you will probably want to specialise. If you’re into verifying functional programs, you should look more deeply at Isabelle’s code generator for instance. If you’re looking at verifying programs written in C, the C-to-Isabelle parser and the tutorial for the AutoCorres tool might be your next stop.

If you are looking for inspiration what to prove, check out the Archive of Formal Proofs to see what small and large theorems others have proved, or check with us over at NICTA’s Trustworthy Systems team for open-source proof projects.