Formalization is rapidly evolving from being highly desirable but thought too difficult to be realistic, to being quite feasible and well on its way to being expected. The raw technology of theorem provers certainly is ready. What is still evolving are the best techniques to apply, and the libraries of “basic” material to support more advanced applications.

Having said that, the task is still not just pure development. Long-term reusability of formal libraries requires sufficient generality, which does not always coincide with easy executability. A careful path of compromise is needed--which is exactly what is done here. While matrix computations are well understood, preexisting work in mathematics (too abstract, so not computable) and in computer science (too low level, albeit extremely efficient, for reuse) is not helpful. A new path is needed.

Here, the authors carefully lay the groundwork for parts of a verified linear algebra library in Isabelle/HOL. Then, they further document how a small network of theories (17, of which 11 are new and described here) help bridge the gap between fields and semirings in such a way that matrices over these domains have good computational and provability properties.

Although the authors are aiming for verified efficient code, they really only obtain half: verified code. By using functional (also known as immutable) data structures, the resulting algorithms are much too memory hungry to be realistic. Granted, what is obtained is considerably faster than what used to be feasible for code verified in this manner--but there is a still a nontrivial gap to bridge.

This is a clear, well-written paper, showing the relentless march forward of science. It’s not a breakthrough, but a carefully constructed building block that can be relied on, with all choices on a twisting, not obvious route documented and justified.