The audience for this superlatively researched and crafted book includes postgraduate students and practitioners of floating-point (FP) computation or formal verification. The authors “sincerely hope that, after reading this book, you will feel like formally verifying your own floating-point algorithms.” Well, I’ve felt like it all my computing life, but this is the first time that I’ll soon dare to do so, with the substantial knowledge and confidence that this authoritative book imparts. (I say this as no stranger to formal methods, but formalizing floating-point computations is where I heretofore have not dared tread.) The Coq [1,2] higher-order logic environment and interactive proof assistant, enhanced by the floqc library that formalizes floating-point arithmetic operations and the Coqueliquot real analysis library (used for numerical analysis), are the main formal methods that underlie this work. These Coq libraries are substantially the work of the (senior) authors, and this book is (also) a high-level guide to their use.
The full import of floating-point data types was brought back to my attention by a relatively recent design review of a safety-critical system wherein loss-of-significance/numerical analysis errors became, by dint of their complex algorithmic nature, substantial hazards alongside the traditional erroneous, ambiguous, or absent specifications and errors in implementation. (The latter were here handled by B and Event-B formal methods [3,4].) Although hazards’ levels of abstraction within a system’s top-to-bottom (and vice versa) design vary, their consequences, namely mishaps, can be catastrophic irrespective of origin.
Of course, computations that yield numerical results preceded digital computers by millennia. Such fundamental notions as the number of significant digits in an intermediate or final result are “classical,” and historical examples of numerical catastrophes (within nominally correct algorithms and calculations) abound. But digital computers engender their own serious pitfalls. For example, a - b + c = a + c - b is true without exception for mathematicians’ and fellow travelers’ integer, rational, real, and indeed complex a, b, c, but fails as a practicable axiom or theorem governing computer hardware, firmware, and programming language software. The book cites, in the introduction, the output of a short C program that witnesses violation of this associativity, here for floating-point numbers. The authors echo computing practitioners’ abiding concern, born of abundant negative experience: “the result of a long computation may be far from the [correct] mathematical result .... This also makes computer arithmetic unintuitive” (to say the least, if I may add).
Chapter 1, on floating-point arithmetic, is one of several individual chapters that are worth the whole price of the book. It is a meticulous, clear, and quite complete explication, via text and efficiently expressive figures, of floating-point arithmetic (mainly if not exclusively in compliance with the IEEE 754 standard).
Chapter 2 summarizes the philosophy and essence of the Coq proof system, but “is not meant to replace the reference manual [COQ 86] or some actual books on the topic.” Though the 11-page references section at the end of the book is quite rich, COQ 86 does not appear there--a minor error.
Chapter 3 treats formalization of IEEE 754 floating-point operations and formats. Roughly half of this chapter, along with chapters 1 and 2, comprises prerequisites for this Master’s/PhD-level book. Formats and types of rounding are cast in natural and also formal (Coq) language. As a side effect that is, again, worth the price of the book, I’ve come to understand IEEE 754 as never before.
Chapter 4, “Automated Methods,” treats (among other things) one of my early holy grails, namely, interval arithmetic. The chapter expounds on Coq’s Gappa tactical tool.
The remaining chapters (5 through 9) are characteristically clear and appropriately detailed expositions of error-free computations, formal proofs of advanced operator properties, compilers and compilation, program verification of C code, and real and numerical analysis of the wave (partial differential) equation.
At the risk of sounding, or even being, pompous, I’ll say that a great book such as this also educates, as opposed to merely training, its readers. Its well-researched choice of Coq leads naturally to the good effects of “reading around one’s subject” [5,6,7]. On a lower level of abstraction, the book precisely expounds the attributes of the C language environments that lead to trusted, well-defined behavior based on formalizing the semantics of source (C) and various target (assembly/machine) languages. In that regard, I was happy to learn more than I had heretofore known about the CompCert C compiler, which implements precise floating-point semantics, as proved with Coq. (The proof of this semantic preservation theorem is covered on page 215.) Ditto regarding the deductive verification Frama-C tool, about which I had heretofore known enough “to be dangerous.”
In summary, this outstanding book has my highest recommendation. The work it describes is a giant step forward in enabling those of us who calculate to be confident of our results, even after hours of silent, unwatched central processing unit (CPU) time.