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.

Coro's concert has now been officially announced. Please buy tickets as soon as you can! The venue is my usual All Saints Ainslie church so the acoustic is good but seating is limited. A particular favourite from the programme this time is Tallis' Lamentations of Jeremiah, which I love singing.

Iustus es Dómine, et rectum iudícium tuum: fac cum servo tuo secúndum misericórdiam tuam.

I am in Edinburgh this week for the combined LFCS/Plotkin/Wadler event so I stopped into my favourite church St. Michael and all Saints to sing in their choir for Mass today. We sang Darke's Mass in F (where I sang the tenor solo), chant propers (which I intoned) and Ola Gjeilo's Ubi Caritas. I linked to our performance in the livestream because SMAS's audio system is quite good and we sang it rather well I think.

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.

I understand my usual choir at All Saints Ainslie sang Pitoni's Cantate Domino.

I also joined the choir at Old St. Paul's for Evensong and Benediction. We sang canticles by Attwood Walmisley (both Magnificat and Nunc Dimittis), and Wesley's anthem Lead me, Lord:

Lead me, Lord.

Lead me in thy righteousness.

Make thy way plain before my face.

For it is thou, Lord,

Thou, Lord, only,

That makest me dwell in safety.