  The Students' Proof Assistant (SPA) aims to both teach how to use a proof
assistant like Isabelle and also to teach how reliable proof assistants are
built. Technically it is a miniature proof assistant inside the Isabelle proof
assistant. In addition we conjecture that a good way to teach structured
proving is with a concrete prover where the connection between semantics, proof
system, and prover is clear. The proofs in Lamport's TLAPS proof assistant have
a very similar structure to those in the declarative prover SPA. To illustrate
this we compare a proof of Pelletier's problem 43 in TLAPS, Isabelle/Isar and
SPA. We also consider Pelletier's problem 34, also known as Andrews's
Challenge, where students are encouraged to develop their own justification
function and thus obtain a lot of insight into the proof assistant. Although
SPA is fully functional we have so far only used it in a few educational
scenarios.
