## 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/

#### Summary

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.**

#### Review

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.

#### References

[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.