ProofBuddy: How it Started, How it's Going
Nadine Karsten, Kim Jana Eiken, Uwe Nestmann
TL;DR
ProofBuddy targets TLPP in CS by replacing local Isabelle installations with a web-based Isabelle backend and an interactive tutorial-enabled interface. Built under an educational design research framework, the authors iteratively designed and evaluated ProofBuddy across multiple WoP iterations (v0–v2), coupling structured tutorials with data collection to study proof competence development. Key contributions include an Isabelle-backed web architecture with a dedicated Isabelle Server Manager, guided tutorials that constrain and scaffold PA usage, and insights into reducing syntax complexity while improving feedback. The work demonstrates that web-based, tutorial-rich tooling can enhance proof pedagogy, offering scalability, standardized environments, and analytics to support large courses, with future plans for learning analytics and tutorial-management tooling.
Abstract
We report on our journey to develop ProofBuddy, a web application that is powered by a server-side instance of the proof assistant Isabelle, for the teaching and learning of proofs and proving. The journey started from an attempt to use just Isabelle in an educational context. Along the way, following the educational design research approach with a series of experiments and their evaluations, we observed that a web application like \ProofBuddy has many advantages over a desktop application, for developers and teachers as well as for students. In summary, the advantages cover simplicity, maintainability and customizability. We particularly highlight the latter by exhibiting the potential of interactive tutorials and their implementation within ProofBuddy.