While the proof interface is still very minimal, my students Josh Brown and Mio Wu have done some amazing work getting the reasoning core of Holbert-ng together. Because I am planning to talk about this work at WadlerFest in two weeks, I began finally to try to realise my original vision for this project and integrate the proof assistant into Forester itself.

It still has some rough edges, but, it works.

In particular, while it's not demonstrated by the above screenshot, proof and definition nodes can span multiple pages, have their own dependency graph (independent of Forester's), can appear in multiple pages, and have all of their state synced to local storage. It's very exciting and motivating to see this in action.

MIHI autem nimis honoráti sunt amíci tui, Deus: nimis confortátus est principátus eórum.

EGO autem sicut olíva fructificávi in domo Dómini, sperávi in misericórdia Dei mei: et exspectábo nomen tuum, quóniam bonum est ante conspéctum sanctórum tuórum.

Inclína Dómine, aurem tuam ad me, et exáudi me: salvum fac servum tuum, Deus meus, sperántem in te: miserére mihi, Domine, quóniam ad te clamávi tota die.

Today our choir at All Saints Ainslie sang for Evensong, so I sang my arrangement of Hildegard of Bingen's O Virtus Sapientiae with a psalm appended during the morning mass. The livestream can be found here:

O Virtus Sapiéntiæ	O Strength of Wisdom!
Quæ circúiens circuísti,	Thou who, circling, hast encircled
Comprehéndendo ómnia in una via quæ habet vitam.	Comprehending all things in the one way that hath life.
Tres alas habens:	Three wings thou hast:
Quarum una in altum volat,	The one which soareth on high,
Et áltera de terra sudat,	The other sweateth from the Earth
Et tértia úndique volat,	And the third flieth everywhere about.
Laus tibi sit, sicut te decet, O Sapiéntia.	Praise be to thee, as is meet, O Wisdom.

In between the morning mass and evensong, I began rehearsing for our next Coro concert. This meant I was singing at the church from morning to night!

For evensong, I selected the music but our normal director conducted. We sang Morley's fauxbourdon Magnificat and Nunc Dimittis, and Tallis' O Lord give thy Holy Spirit as the anthem.

O Lord, give thy Holy Spirit into our hearts,

And lighten our understanding,

That we may dwell in the fear of thy Name,

All the days of our life;

That we may know thee, the only True God:

And Jesus Christ, whom thou hast sent.