my forest
1\date{2025-06-05}
2\author{liamoc}
3\title{Holbert doesn't need to be a document system}
4\p{The existing implementation of [Holbert](https://liamoc.net/holbert) is both a proof assistant \em{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](https://liamoc.net/holbert), which is essentially [our HATRA paper](oconnor-amjad-2022) rendered within Holbert itself.}
5\p{When I converted my [domain theory notes](dt-001Y) to [Forester](https://www.forester-notes.org), the marvellous system from [[jonsterling]] and [[kentookura]], I was able to directly compare the experience of preparing lecture notes in Holbert to Forester, and my conclusion was that Forester is \em{vastly} better for the preparation of lecture notes than Holbert is. }
6\p{This conclusion was based primarily on the fact that, despite their linear presentation, many good lecture notes or mathematical texts are \em{not} lines, where every item depends on all previous items. As the Forester system emphasises, they are in fact a \em{graph} of self-contained notes, which are \em{then} linearised into some sort of narrative order for the sake of explanation or lecture delivery.}
7\p{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).}
8\p{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.}
9\p{This left me with the following conclusions:}
10\ol{
11 \li{\strong{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, \em{embeddable components} (perhaps [Web Components](https://developer.mozilla.org/en-US/docs/Web/API/Web_components)) that can be dropped into any HTML document, including those produced by Forester. }
12 \li{\strong{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.}
13 \li{\strong{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.}
14}