Thinking About Formal Methods

I've been doing a lot of reading lately, especially on different aspects of formal methods and specifications. I like the idea of modeling systems at differing levels of abstraction and identifying problems before a line of code is ever written.

I have started to suspect this particular niche isn't quite so large as other areas of computer science as I plumb the depths of footnotes and references across different texts. This is a bit of a brain dump or mind map of different sources and how they might relate to each other.

Specifying Systems

Leslie Lamport's written introduction to TLA+. I no longer remember where I first heard about Specifying Systems, I do remember thinking the video tutorials from Lamport helped after reading all of part one. Despite reading about the use of TLA+ at Microsoft and AWS I was a little nonplussed on first exposure.

Software Abstractions: Logic, Language, and Analysis

Jackson cites Z as an inspiration for alloy, the language/tool described in the book. I read this after part one of Specifying Systems and liked it better for the fact that it described systems I could understand more readily than message protocols and clocks. With several years to ruminate on things I can see that what Jackson really accomplished was putting Z in a blender with a SAT solver (this is actually a pretty cool feat!).

The Way of Z, Jonathan Jacky

I picked this book up largely because of the subtitle: practical programming with formal methods. I was not disappointed. The book eases through how you might design and model real systems using formal methods without getting bogged down in tooling. As near as I can tell this is because there is vanishingly little tooling for Z.

The Z Notation, A Reference Manual, J. M. Spivey

Definitely not sufficiently motivated for a first book on Z; this is a true reference manual. I found it useful as a way to get a less opinionated view of Z than that provided by Jacky

Programming and Mathematical Thinking, Alan Stavely

Subtitled A Gentle Introduction to Discrete Math Featuring Python this is one that I have come to appreciate. I think the author taught undergraduates and the coverage feels aimed at about that level. Still, it is one of the few books I have come across that really nails the subject matter in a way that leaves me feeling like I've immediately learned something practical. Re-reading this book after more abstract texts like those above I have a better sense of how I might translate a formal specification into a running program while maintaining the mathematical rigor.

Toward Zero-Defect Programming, Alan Stavely

Another re-read for me and another by Stavely. I don't think he ever explicitly mentions formal methods, instead focusing on clean-room programming, but the method described is a practical approach to turning specifications into working code without introducing bugs along the way.

A Programming Language

Iverson's book introducing the notation (APL) before an implementation even existed. I read this and was blown away at the idea of creating an entire language before implementing it. Similarly compelling is the idea of a language that precludes entire classes of bugs by virtue of the paradigms used.

Introduction to the Theory of Programming Languages, Bertrand Meyer

Wondering how you design a language with sound fundamentals (rather than by accident) I picked this up and really struggled with it. It wasn't until reading about Z and coming to grips with some of the notation that Meyer's metanot started to click for me and I began to focus on the subject matter. Especially useful beyond the realm of just programming languages is the coverage of axiomatic semantics. By understanding the sorts of theorems and proofs covered here it has begun to feel like I can see the real-world use of formal system descriptions.

A formal description of SYSTEM/360 (doi:10.1147/sj.32.0198)

From a 1964 IBM Systems Journal, it describes the SYSTEM/360 using Iverson's notation (APL). This one is interesting partly because of the brevity and partly because it doesn't really feel so old. Comparing this to something like a recent specification using TLA+ for Azure Cosmos DB is especially mind-bending for me personally. Nearly 60 years and we're still only scratching the surface!

Warren’s Abstract Machine, A Tutorial Reconstruction

Warren's Abstract Machine (WAM) is a popular design for implementing a Prolog virtual machine. This book is a gradual, explicit justification for the design of WAM. There are surprisingly few resources for learning about real world virtual machines, this book is a generally readable explanation even for a layman such as myself.

Coalton

a statically typed functional programming language built with Common Lisp. I think I first found Coalton during a search rabbit hole for the intersection of programming languages and Common Lisp. Reading about Coalton led to a few questions about SML as it is the only real exposure I have to Hindley-Milner type systems.

The Definition of Standard ML

a rigorous formal definition of Standard ML written by the language creators. I found it even more mathematically rigorous than something like R4RS which was probably the most stringent language document I had previously read.

ACL2

I found ACL first mentioned in the acknowledgments of the above post about Coalton. ACL is a logic prover built on Common Lisp and used in industry. I read the tutorials and mentally slotted this in the same space as the TLA+ checker and Alloy; interesting but not too compelling for me personally.

A Verified Prolog Compiler for the Warren Abstract Machine

I found this in a footnote in the WAM book and I suddenly had a connection between this, the WAM book, and these other items. There are relatively few full specifications or proofs for real-world systems and fewer still so thoroughly explained.

Formal Verification of Floating-Point Hardware Design

While browsing around the website of the WAM verification's author I noticed he has recently (2018) published a book on formal verification in the context of hardware design. Digging into the details I realized the proofs were all constructed in ACL2! The circularity of my footnotes deepens. Clocking in at nearly 400 pages of mathematical proofs, I would deem this a pretty "hard core" book. The first two chapters however have proven approachable.

If I ever finish reading all of this and can stomach any more on the subject of formal methods I might turn to Modeling in Event-B: System and Software Engineering, which is apparently a method in the lineage of B (and Z) designed to be computer-assisted but easier to learn and focused on refinement into working programs. Additionally, I want to learn more about seL4 which is a microkernel first proven correct with a machine checked proof and then translated to Haskell and then translated to C, all while maintaining the proof of correctness. While there are a series of wiki pages, tutorials and reference manuals there doesn't seem to be an obvious "start here".

I think in a few more years I might make some sense of all of these things; for now all this reading only slowly illuminates things.