The existing implementation of Holbert is both a proof assistant and a document preparation system. The vision was that my lecture notes (or even a full textbook) could become an interactive learning medium, where exercises can be completed right from the same browser window used to read the lecture notes. This can be seen in action in the default Holbert document, which is essentially our HATRA paper rendered within Holbert itself.
When I converted my domain theory notes to Forester, the marvellous system from Jon Sterling and Kento Okura, I was able to directly compare the experience of preparing lecture notes in Holbert to Forester, and my conclusion was that Forester is vastly better for the preparation of lecture notes than Holbert is.
This conclusion was based primarily on the fact that, despite their linear presentation, many good lecture notes or mathematical texts are not lines, where every item depends on all previous items. As the Forester system emphasises, they are in fact a graph of self-contained notes, which are then linearised into some sort of narrative order for the sake of explanation or lecture delivery.
Holbert, like most proof assistants, views a document as a linear script with a strict top-to-bottom dependency order. Forcing this to be the layout of the document unnecessarily constrains writing and makes multi-document developments a difficult implementation challenge (and one that Holbert never managed to achieve).
Furthermore, the editing experience when writing prose in a Holbert document is significantly clunkier than Forester. Normal text editors and version control can't be used, making collaboration difficult. The markup format for paragraph items was vaguely similar to org-mode but different enough to make writing it confusing. The structural editor for proofs and rules doesn't assist at all when writing prose. There is no way to define macros, and no good way to cross-reference other parts of the text.
This left me with the following conclusions:
- Holbert should get out of the business of preparing documents. Systems like Forester already do that job excellently. Instead, the next version of Holbert should consist of modular, embeddable components (perhaps Web Components) that can be dropped into any HTML document, including those produced by Forester.
- Holbert should abandon linear dependency graphs. The dependencies between the embeddable components are graphs, not lines. The order of presentation in a document should be decoupled from the dependency graph of the Holbert components. In addition, not all dependencies of a component need occur on the same page.
- Holbert should have a text-based format as well as a graphical one. The graphical proof and rule editing is nice, but it's not amenable to version control or editing outside of Holbert. The next version of Holbert should support a textual format from the ground up.