Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan: Functional Algorithms, Verified!
Freely downloadable: https://functional-algorithms-verified.org/
The book Functional Algorithms, Verified! presents a number of classical functional data structures, accompanying each of them with formal specifications. These specifications describe both the functional correctness and the time complexity of every operation, emphasizing the notion of interface for an abstract data type. The book can be seen as a way to augment a course on functional data structures with an introduction to formal specifications.
This review is written by Arthur Charguéraud for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community.
Functional Algorithms, Verified!
by Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan.
The book Functional Algorithms, Verified! provides a presentation of classic functional data structures and algorithms with a fairly original perspective: that of accompanying every data structure with formal specifications. The specifications cover not only functional correctness, but also time complexity bounds. The book has been used as course notes by Tobias Nipkow and colleagues over several years. It benefits from feedback from the classroom, invaluable for streamlining the presentation of the material. I would say that it is well-suited for master’s students. It could also be accessible for students in the final year of a bachelor’s degree, and highly valuable to PhD students who wish to formalize or use formalized data structures.
Interestingly, although its contents are formally verified, this book is not about mechanized proofs. It is meant to be accessible to readers with no background in proof assistants. What matters in this book is the mechanized specifications, which are provided for every data structure. Throughout the book, the reader is taught how to write formal specifications for sets, maps, sequences, functional arrays, and priority queues. These formal interfaces are the cornerstones of program verification. The proofs are presented in English, each time with formal statements and an explanation of what kind of induction principle is exploited. The proof details, which can be found in the accompanying Isabelle/HOL proof scripts, are very useful for readers interested in conducting formal proofs on functional data structures. For other readers, following the proof scripts is completely optional.
The book begins with list sorting algorithms, then covers a fair number of binary trees that implement search trees and priority queues, and includes specific chapters on the notions of dynamic programming, of amortized analysis, and, most importantly, of abstract data type (ADT). Compared with Chris Okasaki’s masterpiece, Purely Functional Data Structures [Oka99] , the present book is less ambitious in terms of contents and amount of explanations. However, it goes much further in terms of formalism—this is the whole point of the book. Even though the present book is self-contained, I would nevertheless recommend a student to study Functional Algorithms, Verified! in parallel with Okasaki’s book and, for the relevant chapters, with the reference book Introduction to Algorithms [CLRS22]. This would provide the reader with the rationale underlying each data structure, then allow them to see how paper-and-pencil statements can be converted into machine-checked definitions.
The book Functional Algorithms, Verified! presents the code and its specifications using the syntax of Isabelle/HOL, which is not far from the syntax of Haskell. The authors were nevertheless careful to choose only a subset of the syntax, making the book, I found, an easy read for a programmer familiar with the syntax of OCaml and/or Coq. For a similar course based on Coq, one might be interested in the course Verified Functional Algorithms (VFA), Software Foundations Volume 3, designed by Andrew Appel [App21]. How does the present book compare against VFA? On the one hand, the present book does not teach how to carry out mechanized proofs. Instead, it presents proofs in plain text, simply exposing the key ideas from the mechanized proofs, which are available in a separate script. On the other hand, the present book covers a larger number of data structures, and, quite importantly, systematically covers the complexity analysis aspects.
Regarding complexity analysis, the book presents, for each data structure, formal bounds for the costs of its operations. Certainly, this material is a key added value of the book. Even though most of the mathematical bounds have been known for decades, the formalization of several of them has only recently been achieved. The bounds are generally not stated using the big-O notation, but using concrete constant factors, a deliberate choice to avoid technicalities. I totally approve of this choice, because state-of-the-art tools are not yet mature enough for students to conduct interactive proofs using the asymptotic big-O notation.
The complexity bounds are established with respect to cost functions that are constructed following the structure of the code. Although the construction follows a fairly systematic pattern, the cost functions are written by hand in the Isabelle/HOL script. Perhaps in the future the cost functions could be automatically generated from the source code, or at least could be somehow formally related to the source code. That said, compared with books that provide no formal specifications and no mechanized proofs at all, the added value of the present book is huge.
The book focuses on functional data structures. The choice of this scope immediately raises the question: what about imperative data structures? There would certainly be a strong need for a follow-up book—who knows, I might contribute to such a book. One thing is certain: learning how to verify functional data structures is an essential first step. In my experience, when verifying, say, an imperative tree data structure, at least three fourths of the work consist of providing the arguments justifying the correctness and the complexity of the operations on the corresponding purely functional tree. In summary, even though the book is focused on purely functional data structures, I would strongly recommend it also to someone interested in verifying imperative data structures.
For many teachers, finding the time to introduce their students to formal specifications is very challenging, because there are already so many aspects of computer science that need to be covered. The book Functional Algorithms, Verified! might offer an anwser. It provides the means to introduce, as part of a course on functional programming and/or as part of a course on data structures, the key concepts of formal specifications. Indeed, functional data structures provide a very interesting collection of examples on which to practice the writing of formal specifications. Obviously, the book might also be used as part of a proper course on formal methods, especially for a light course that focuses on specifications and does not dive into the details of interactive proofs. Regardless of their motivation, external contributors are welcome by the authors to contribute to developing the book further.
[App21] Andrew W. Appel. Verified Functional Algorithms, volume 3 of Software Foundations. Electronic textbook, 2021. Version 1.5.1, http://softwarefoundations.cis.upenn.edu.
[CLRS22] Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to algorithms. MIT press, 2022. Fourth edition.
[Oka99] Chris Okasaki. Purely functional data structures. Cambridge University Press, 1999.