Introduction to Verification with the Coq Proof Assistant

Despite our best efforts, even well-typed functional programs still contain bugs that might or might not be uncovered by the tests. Wouldn’t it be nice if we could prove the correctness from mathematical foundations instead? Interactive proof assistants such as Coq allow you to write a correctness specification in mathematical logic, implement the program in a statically-typed functional language and argue for the correctness as part of the implementation.

This tutorial shows how to start using one specific proof assistant, the Coq proof assistant, by leading through a row of examples over inductive data structures. Programs are written in an OCaml-like language, while proofs are constructed using so-called tactics that allow developing indisputable proofs in an interplay between humans and computers.

Basic familiarity with writing programs in (any) functional language helps follow this tutorial. No further knowledge is required.

Tutorial preparation

Before the tutorial, please have an IDE for Coq available. There are two recommended possibilities:

• You can install the Coq proof assistant together with CoqIDE. See here for complete download instructions. See here for binary installers for Coq 8.14.1 for macOS/Windows and here for Linux. For simplicity, we use the CoqIDE, but interfaces for EMacs and Visual Studio Code are available.

• You can run Coq in your browser via the jsCOQ plugin.

Kathrin Stark

@KathrinStarkCS

Kathrin Stark recently started as an assistant professor in computer science at Heriot-Watt University in Edinburgh. She started using proof assistants after attending a lecture ten years ago and has been a user of the Coq proof assistant ever since. In her research, she works on minimising the overhead in using proof assistants and on turning them into a practical software verification tool.