My honours students have been hard at work on the next generation of Holbert lately. Mio Wu has finished implementing an engine (including pattern unification) for higher order terms, and is now investigating Functions-as-constructors higher-order unification for implementation in Holbert-ng. Also Josh Brown has been looking into E-unification modulo associativity, so that we can represent syntax and parsing rules in Holbert. Both have made excellent progress, with basic versions of their respective unification algorithms already in place and working.
I'm hoping that I will have time to work on the UI side of things again sometime in September, but we shall see!