We now have the field of Explainable AI to explain to us why this #@%$& autopilot wants to stop in the middle of the road for no apparent reason. I'd like to propose a new field, the field of Explainable Program Proof, as the subject of the very recently published book Program Proofs by well-known researcher Rustan Leino. After all, the automatic provers at the heart of program proofs are a kind of artificial intelligence (not based on deep learning), one that very much surprises developers sometimes when the analyzer figures out something they did not think about. And like the more popular form of AI, it can be #@%$& difficult to understand why the analyzer fails when it fails.

The goal of that book is to guide you through the use of program proof using the Dafny language and analyzer that Rustan started developing at Microsoft Research and now continues developing at the Automated Reasoning Group of Amazon Web Services. I find it very nice that the first half of the book is devoted to proving functional programs (one of the programming styles in Dafny) before entering the proof of imperative programs (also possible in Dafny) in the second half. This is because reasoning about mutable state is hard, and harder than what developers think initially. With this choice of presentation, you get a chance to perform reasonably advanced proofs before you even have to look at the misery of applying these techniques to imperative programs.

You don't have such luxury in SPARK, but the distinction between functional and imperative parts is still very useful, as contracts (code for specification) and ghost code (code for verification) are typically functional in nature, while the program is imperative. And you can of course, do the same program proofs in SPARK as the ones in Dafny presented in the book, which you'll find on this dedicated GitHub project.

That was quite a wait since I first got excited by the draft of the book almost exactly 3 years ago! At the time, I said to Rustan:

We badly need your book to answer all the users who are asking for "proof tips", trying to fast-forward their proving capabilities by relying on a digest of our expertise.

I think the book provides exactly that. Whatever program-proof technology you're using. I definitely recommend it to all SPARK programmers.