Javier Casas

A random walk through computer science

Book review: The Little Prover

I just finished reading "The Little Prover". It's a small introduction to proving programs using formal methods, in this case, rewriting programs using axioms or proven theorems.

As you can read on other websites, the book is said to be "mind bending", and that's probably the best description I have for it. It teaches complex proofs in an affordable way, having to provide only lots of time and patience. As you go through the chapters, the complexity slowly ramps up. Whereas the first chapters explain everything up to the minimum detail, the later chapters start to skip details that should be obvious once you start to understand the main themes, and start to learn the axioms. Eventually, you reach a point where you understand enough of the materials to actually attempt and succeed at some proofs on your own.

The pains

The proof checker - J-Bob - is somewhat helpful, but the book would be less painful if it taught you beforehand how to make it help you. The first thing you need is the right shape for the commands:

(defun name-to-identify-chapter ()
  (J-Bob/prove (function-that-provides-axioms)
               '(
                 ((dethm theorem-name (x)
                         (equal (align (align x)) (align x)))
                    
                  (measure)
                  ((A 1 1) (align x))
                  ((A 2) (align x))
                  (other-steps-here)
                  )))

Without this, it's too tempting to use J-Bob/step, which is actually a pain to use. With J-Bob/prove you can see your progress, and when you are finished, you replace J-Bob/prove with J-Bob/define and you are ready to use the proof you just formulated.

The other part that J-Bob desperately needs is a way to illuminate the section you are rewriting. When you are writing (E A A 1 A 2 1) you don't know if the position is right, or how many elses you have already skipped. The system isn't very hepful, as if you target the wrong element, it doesn't rewrite anything, showing the previous result. In big expressions it may be hard to make sense if the expressions has been rewritten or not, specially after each rewrite can construct a new expression that may be rendered in a subtly-different way.

The gains

J-Bob may be a bit harsh on the practicioner, but using it helps a lot. Specially if you use it in Racket or other envionment that helpfully points starts and ends of expressions, and indents nicely. On the journey you will practice a lot of grunt-work designed to help you understand how can you prove stuff. Soon you will know by heart the main axioms (if-same, equal-same, car/cons, cdr/cons, if-nest-A, if-nest-E) and they will begin to be your second nature. You will grow to understand the basics of formal proofs, and I'm sure it will help you understand how you can refactor code, as each rewrite essentially constructs the same expression but with different shape. You will also learn the importance of reversing some rules, and how you can create some elements out of thin air. It's some kind of magic.

Recap

This is one of those books you need to read to start grasping the theory behind proofs, as well as to start applying it. It is not very long, but practicing all the chapters gets a bit long, specially until you get the hang of it. The results will be great for your brain, as you will learn a lot about proving programs to be correct and total, and will practice the art of understanding big s-expressions in order to target the element you want to rewrite. Totally recommended.

Back to index