Holbert: Reading, Writing, Proving and Learning in the Browser

TL;DR

Holbert is an online platform combining a pedagogical proof assistant with a textbook interface, designed to facilitate teaching programming language theory through interactive proofs and rule manipulations.

Contribution

It introduces a novel integrated online textbook and proof assistant system tailored for educational purposes in programming language theory.

Findings

Prototype implementation demonstrated proof manipulation in-browser

Interactive exercises enhance learning engagement

System supports embedding proofs directly in textbooks

Abstract

This paper presents Holbert: a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status.