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:

1. 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.
2. 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.
3. 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.

The current Holbert implementation is written in Haskell and the miso framework, and compiled to JavaScript using ghcjs. This has many obvious drawbacks: 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 massive blob of JavaScript code, the performance of which isn't great; and interop with existing web infrastructure is difficult at best.

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.

Even worse, the kind of code for which purely functional languages like Haskell excel (term manipulation etc.) makes up only a 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 library for Haskell, but this severely limited my ability to get students collaborating with me on the project.

Most undergrad students at the University of Edinburgh or the Australian National University 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.

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.

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 § [loc-000W].

So, the conclusions I'm left with are:

1. 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.
2. The codebase should be understandable by an undergrad. I will intentionally avoid "fancy stuff", even if it means writing some more boilerplate.
3. The build toolchain for Holbert should be easy to set up. ghcjs is definitely not this, and it's a pain.