Verification used to be a daunting task, to be performed only in extreme circumstances, at great cost. Our knowledge of how to perform verification, at least for certain kinds of code, has progressed so much that there are now textbooks, accessible to undergraduate students, on how to do it. And this is one such textbook. It is engagingly written and pleasantly weaves together two strands: how to write functional code, and how to prove properties about functional programs.

This is not a whimsical choice because many of the most effective techniques require back-and-forth between proofs and code. The tool of choice here is Agda (there are other excellent textbooks that choose Coq instead). The author makes sure to introduce important aspects of Agda as he goes along, without losing sight that verification is the main goal. Some important points are made, such as the difference between internal and external verification. The topics, and their progression, are also consistent with the aims of the book.

The author makes one unusual choice: rather than relying on the (albeit complex and sometimes weirdly organized) standard library, he provides an alternate library. Some of his definitions seem awkward, such as using classical Booleans for relations and then having to write a < b ≡ true instead of defining relations as returning proof objects. This makes certain things feel more immediately computational at the cost of awkwardness in certain definitions and proofs. Of course, the standard library has its own share of awkward corners, just in different places.

If someone is picking up this book to understand how Agda’s creators use Agda, they will be disappointed. However, this does not really distract from the main thrust of the book, Agda-assisted program verification. Here, the book is excellent. And it is accessible to undergraduates, which is no mean feat. If your aim is to learn (or teach) verified functional programming, I would definitely recommend this book.

More reviews about this item: Amazon