  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.
