+7

trees/loc-000V.tree

reviewed

··· 1 1 + \title{Rethinking Holbert} 2 2 + \date{2025-06-05} 3 3 + \author{liamoc} 4 4 + \p{As is clear to anyone who has been following development, progress on my in-browser proof assistant [Holbert](https://liamoc.net/holbert) first slowed to a trickle, and has now completely stopped. Unlike some other projects of mine that have dried up, this is not due to any loss of interest in the project on my part, but rather deep-seated technical and design issues that have prompted a rethinking of the project.} 5 5 + \p{Starting soon this year, I intend to begin a rewrite of the Holbert project, although with a different focus and with a vastly different implementation strategy. This note serves as both a retrospective on the current Holbert implementation and a vision for the next iteration of the Holbert idea.} 6 6 + \transclude{loc-000W} 7 7 + \transclude{loc-000X}

+14

trees/loc-000W.tree

reviewed

··· 1 1 + \date{2025-06-05} 2 2 + \author{liamoc} 3 3 + \title{Holbert doesn't need to be a document system} 4 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 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 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 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 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 9 + \p{This left me with the following conclusions:} 10 10 + \ol{ 11 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 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 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 14 + }

+15

trees/loc-000X.tree

reviewed

··· 1 1 + \date{2025-06-05} 2 2 + \author{liamoc} 3 3 + \title{Holbert shouldn't be written in Haskell} 4 4 + \p{The current [Holbert](https://liamoc.net/holbert) implementation is written in Haskell and the [miso](https://haskell-miso.org) framework, and compiled to JavaScript using \code{ghcjs}. This has many obvious drawbacks: \code{ghcjs} is stuck on an outdated version of GHC Haskell (although the GHC JavaScript backend has been ready for use "any day now" for the past couple of years, it doesn't seem to be picking up major traction); it generates a \em{massive} blob of JavaScript code, the performance of which isn't great; and interop with existing web infrastructure is difficult at best.} 5 5 + \p{The initial reason for this choice is that my initial implementation used Huet's higher order unification algorithm, and lazy evaluation makes this significantly easier to code up. But ultimately we switched Holbert to use pattern unification instead, and so the initial reason for using Haskell evaporated. } 6 6 + \p{Even worse, the kind of code for which purely functional languages like Haskell excel (term manipulation etc.) makes up only a \em{minority} of the total code in Holbert, with the majority being UI code and code to update deeply-nested data structures. Vanilla Haskell is notoriously bad at this, so to cut down on boilerplate, I used the [optics](https://hackage.haskell.org/package/optics-0.4.2.1/docs/Optics.html) library for Haskell, but this severely limited my ability to get students collaborating with me on the project. } 7 7 + \p{Most undergrad students at the [[uoe]] or the [[anu]] will have seen Haskell, but only the nice parts covering functional programming with algebraic data types and very basic IO. Many wouldn't really have seen monad transformers, and none would have seen lenses or optics before. So, by using these more advanced features extensively in the Holbert code base, I was more-or-less guaranteeing that the only person able to work with that code-base would be me.} 8 8 + \p{It's also painfully obvious that Haskell is not a language for the web. The intersection of skilled Haskell programmers and skilled web programmers is pretty small, so I end up with few people who can make meaningful contributions to the project.} 9 9 + \p{I'm also starting to think that a more object-oriented, bottom-up data model of a Holbert document would make more sense. Rather than conceive of a document as a list of items, and using optics to drill down to one particular item and make changes, I think a better model would be for each Holbert component to be like a process, responsible for managing its own state and communicating changes to any components that depend on it. This ties in well to the graph-orientation I discuss in \ref{loc-000W}. } 10 10 + \p{So, the conclusions I'm left with are:} 11 11 + \ol{ 12 12 + \li{\strong{The UI part of Holbert, at least, should be written in a web-friendly programming language.} If necessary, the unification and term manipulation parts could be written in a more functional language and imported, but I'd only do this if it were truly painful to write the whole thing in one language.} 13 13 + \li{\strong{The codebase should be understandable by an undergrad.} I will intentionally avoid "fancy stuff", even if it means writing some more boilerplate.} 14 14 + \li{\strong{The build toolchain for Holbert should be easy to set up.} \code{ghcjs} is definitely not this, and it's a pain.} 15 15 + }