Carnap Ten Years Later: Lessons Learned and Next Steps

Graham Leach-Krouse

Carnap Ten Years Later: Lessons Learned and Next Steps

Logic in Computer Science 2026-07-04 v1 Software Engineering

Authors: Graham Leach-Krouse

Abstract

The first part of this paper provides an experience report, recounting the design and long-term maintenance of the Carnap proof assistant framework used cumulatively by over 45,000 students worldwide over the last decade. We cover the good, the bad, and the ugly: what worked well, what didn't work, and what added friction to development and maintenance over time. These insights motivate a bottom-up redesign of the Carnap framework, which is the topic of the paper's second part. Briefly, the new design combines a new high-performance verifier kernel (mm0-zig) targeting Mario Carneiro's metamath zero format, and the Aufbau Bytecode Compiler, (abc), a new proof compiler that can serve as a backend for richly interactive proof-authoring experiences on the web.

Cite

@article{arxiv.2607.07722,
  title  = {Carnap Ten Years Later: Lessons Learned and Next Steps},
  author = {Graham Leach-Krouse},
  journal= {arXiv preprint arXiv:2607.07722},
  year   = {2026}
}

Comments

11 pages, 2 figures, 1 table. Accepted for publication at TEAL