More Pie for the Little Typer: Accessible, Extensible, and AI-Guided Proof Education
Abstract
Pie, the dependently typed teaching language of The Little Typer, is pedagogically near-ideal: just enough to teach dependent types and proof, and no black boxes. Yet its original implementation imposes barriers of its own: a heavyweight local setup, no interactive feedback, a fixed set of built-in types, and proofs written as flat terms with no goal-directed workflow. We reimplement Pie from scratch in TypeScript and add three extensions that make it more accessible and extensible for learners. Tactics build proofs by goal-directed steps yet extract an ordinary, reusable term; named holes extend Pie’s single unnamed placeholder so that several open goals can each report their own type and context; and user-defined inductive types come with automatically generated eliminators. An interactive proof canvas renders these tactic proofs and lets a learner build them by direct manipulation. On this core we add PieLoT, an AI assistant: a self-supervised fine-tuned tactic predictor and a Socratic hint service that explains rather than solves. We report the design, worked examples, and a preliminary evaluation of how the system overcomes the limitations of Pie’s original implementation. The result is a browser-based, extensible, AI-guided proof environment built on a minimal, transparent core.
