Holbert-ng nearing readiness [loc-005E]

September 6, 2026
Liam O'Connor

I said in my last post that proof interface still needed work for Holbert-ng to reach feature parity with Holbert 1, but being sick with COVID meant that suddenly pressing work commitments vanished and I stayed home to isolate myself. This gave me a lot of programming time, so now a preliminary release of Holbert-ng is imminent.

The real test will be to actually start writing my PL course notes (similar to my domain theory notes but more for an undergraduate PL theory course) with the proof assistant integrated throughout, as per my original vision. We're now almost at a point where that is a feasible thing to do. I will give a talk about some of my design decisions at the Wadler 70 event on Wednesday.

Ubi cáritas et amor, Deus ibi est.	Where there is charity and love, there God is.
Congregávit nos in unum Christi amor;	The love of Christ has gathered us as one;
Exultémus et in ipso iucundémur;	Let us then exult and delight in him;
Timeámus et amémus Deum vivum,	Let us fear and love the living God,
Et ex corde diligámus nos sincéro.	And love each other with sincere hearts.
Ubi cáritas et amor, Deus ibi est.	Where there is charity and love, there God is.
Amen.	Amen.

$\pi _0 \circ \langle f , g \rangle = f$
$\pi _1 \circ \langle f , g \rangle = g$
$\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h$


( $y \mapsto b \mapsto z$ but $z \not \sqsubseteq y$ )	( $b \mapsto x \mapsto a$ but $a \neq b$ )