# Students' Proof Assistant (SPA)

## TL;DR

SPA is an educational tool that teaches students how to use and understand proof assistants by providing a miniature proof assistant within Isabelle, emphasizing the connection between semantics, proof systems, and proof development.

## Contribution

It introduces a miniature proof assistant inside Isabelle to facilitate teaching structured proving and understanding proof system reliability, with practical comparisons to existing proof assistants.

## Key findings

- SPA effectively demonstrates proof structures similar to TLAPS and Isabelle/Isar.
- Students gain insight by developing their own justification functions.
- SPA has been successfully used in educational scenarios.

## Abstract

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.