Once there was a series of books on Scheme, starting from "The Little Schemer" by Friedman. It taught how to understand and construct a Scheme interpreter in a very peculiar manner of atomic questions and answers, making a whole book one huge dialogue.

This one is similar, only now the subject is a minimalistic Dependently-Typed prover, which shifts the dialogue quite soon towards hardcore (since the topic itself is rather hard).

The prover described itself does exist, been developed in Racket by the authors. Great example of interactive system, and a nice first dive into Formal Verification area. And the illustrations are awesome, as before!