This forest has now been ported to Forester 6.0. You may need to clear your cache to get rid of stale stylesheets or redirects. Despite the fact that the HTML backend of Forester 6.0 doesn't support any customisation, I was able to inject my customisations including Gregorian chants, syntax highlighting, TSV tables and most of my style tweaks simply by making a custom Forester 6.0 theme that replaces the existing style.css with a file that @imports my additional style sheets, and similarly the min.js with a file that imports all of my custom scripts.

There were a few bugs or minor things that I had to fix, that I'll document here:

• The new search dialog looks for forest.js in the wrong place, so I hardcoded a fix for my forest in my custom theme.
• The generated pages preload katex.min.css but don't actually load it. I put a @import(katex.min.css) line into my stylesheet to fix this.
• The generated index.html redirects to the wrong place, so I put a custom index.html in the custom theme that overrides Forester's generated one.
• The top-level .block elements in a page didn't have the data-taxon attribute which my custom stylesheet depends on. I guess this is also a bug, as it's a regression from the previous Forester 5.0 pages. I added this to the Forester source code in my private fork.
• The download link meta-data that I added custom to my XSLT sheet in Forester 5.0 is now hardcoded in my private fork of Forester 6.0. Perhaps when more customisation options are added (and the above bug fixed), I will not need a private fork anymore, as this is really the only customisation I had that cannot already be accommodated by my custom theme.

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

Ego clamávi, quóniam exaudísti me, Deus: inclína aurem tuam, et exáudi verba mea: custódi me, Dómine, ut pupíllam óculi: sub umbra alárum tuárum prótege me.

This morning at All Saints Ainslie we sang Be still for the presence of the Lord, which is way too 1980s for my taste but it is what it is:

Be still, for the presence of the Lord,

the Holy One is here.

Come, bow before Him now,

with reverence and fear.

In Him no sin is found,

we stand on holy ground.

Be still, for the presence of the Lord,

the Holy One is here.

Be still, for the glory of the Lord,

is shining all around.

He burns with holy fire,

with splendor He is crowned.

How awesome is the sight,

our radiant King of Light!

Be still, for the glory of the Lord,

is shining all around.

Be still, for the power of the Lord,

is moving in this place.

He comes to cleanse and heal,

to minister His grace.

No work too hard for Him,

in faith receive from Him.

Be still, for the power of the Lord,

is moving in this place.

We chose this anthem because our original plan was too ambitious, and we had sung this anthem the day before at the wedding of Sajay (one of our choristers) and Jaclyn, along with Bob Chilcott's Be thou my vision.

Si iniquitátes observáveris Dómine, Dómine quis sustinébit? quia apud te propítiatio est, Deus Israel.

This morning at All Saints Ainslie we had a very small choir so we sang some established repertoire with me as the only tenor and our director managing the soprano part, Byrd's Ave Verum Corpus:

Ave verum corpus natum de María Vírgine,	Hail, true body, born of the Virgin Mary,
Vere passum immolátum in cruce pro hómine,	True suffering, sacrificed on the cross for Man,
Cuius latus perforátum unda fluxit sánguine,	From whose pierced side flowed waves of blood,
Esto nobis prægustátum in mortis exámine.	Be for us a foretaste in death's trial.
O dulcis, O pie, O Iesu fili Maríæ,	O sweet! O blessed! O Jesus, son of Mary,
Miserére mei, miserére mei, miserére mei.	Have mercy on me, have mercy on me, have mercy on me.

OpenAI have foisted upon the mathematical community a dump of hundreds of new "results" in mathematics, excreted by their machines. I hope it goes without saying that this is a disgusting abuse of the mathematical community and the intellectual commons. I refer to the statement by the Association for Human Mathematics:

Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power. We urge mathematicians to discontinue their work with OpenAI and to return to a vision of science that centers human understanding.

I also quote Antonio E. Porreca from his excellent reaction to this:

I believe that we, as researchers and teachers, must reject AI-powered “papers” like these as legitimate research, because they’re not. And even if they were, it’s research that’s not worth doing. It does not follow any of the rules or the values of academia: building on the work of others with citations, not scooping your colleagues, collaborating, learning, teaching… and, you know, actually writing your own stuff in good faith. We have a right not to read papers like these, we have a right, no, a duty, not to cite them, to refuse refereeing them.

Even if you, as a “senior” (meaning, with a permanent academic position) believe that it’s OK for yourself to do AI-powered “research”, you should think about your students and your junior and future colleagues. AI-powered “research” is not self-sustaining: you will always need a human expert in the loop, even if it’s just for asking question to your LLM chatbot, filtering all bullshit answers, and interpreting and applying the result (a job I wouldn’t wish on my worst enemy). If AI-powered “research”, let alone “teaching”, becomes the norm, we’ll lose at least a generation of human experts. I’ve personally witnessed whole classes of students pressured (by peers and, above all, by the behaviour of their teachers and the university bureaucrats) into using LLMs to write code. These students are not learning. They will never be the human expert in the loop. And the same thing will happen to our junior colleagues, if you force them to use LLMs to do their job. In fact, one day there will be no expert at all. Even if you don’t believe that, one day you will lose your expertise too if you let LLMs do your science for you. Snap out of it.

In voluntáte tua, Dómine, univérsa sunt pósita, et non est qui possit resístere voluntáti tuæ: tu enim fecísti ómnia, cælum et terram, et univérsa quæ cæli ámbitu continéntur: Dóminus universórum tu es.

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 tuorum.

This morning I sang with a skeleton crew choir at All Saints Ainslie, for an, uh, interesting service replete with all the dogs of the congregation. The animal blessing itself was a bit too Common Worship for my taste, but it was nice to see all the cute animals. We sang Brother James' Air:

The Lord's my Shepherd, I'll not want.

He makes me down to lie

In pastures green; He leadeth me

The quiet waters by.

He leadeth me, He leadeth me,

the quiet waters by.

My soul He doth restore again;

And me to walk doth make

Within the paths of righteousness,

Ee'n for His own Name's sake.

Within the paths of righteousness,

Ee'n for His own Name's sake.

Yea, though I pass through shadows death,

Yet will I fear no ill;

For Thou art with me; and Thy rod

And staff me comfort still.

Thy rod and staff they comfort still

They comfort still.

My table Thou hast furnishd

In presence of my foes;

My head with oil thou dost anoint,

And my cup overflows.

My head thou dost with oil anoint,

And my cup overflows.

Goodness and mercy all my days

Will surely follow me;

And in my father's heart alway

My dwelling place shall be.

We (being Coro) performed to a sizeable but not sold-out crowd for our second concert of the year, Cloudburst.

I really enjoyed working with our guest director, Roland Peelman, and it was great to have the opportunity to sing Tallis' Lamentations of Jeremiah (Part 1 and Part 2).

The full programme is outlined in this review from Jacqui Smith at classikON.

What a treat to hear a new choir (for me) performing such a profound and deeply moving program, with excellent artistic programming, pace and delivery. I can’t wait to hear what they sing next.

There was also a more nitpicky review on CityNews.

I'll likely be singing again with a subset of Coro for a special Christmas concert. Stay tuned!

Benedícite Dóminum, omnes Angeli eius, poténtes virtúte, qui fácitis verbum eius, ad audiéndam vocem sermónum eius.

In nómine Dómini omne genu flectátur, cæléstium, terréstrium et infernórum: quia Dominus factus obédiens usque ad mortem, mortem autem crucis: ídeo Dóminus Iesus Christus in glória est Dei Patris.

Omnia quæ fecísti nobis, Dómine, in vero iudício fecísti, quia peccávimus tibi, et mandátis tuis non obedívimus: sed da glóriam nómini tuo, et fac nobíscum secúndum multitúdinem misericórdiæ tuæ.

This morning I was groggy after a night at the German club after my Cloudburst concert had wrapped up, but still cantored at All Saints Ainslie in a duet with our director Alasdair, singing Dering's Duo Seraphin:

Duo séraphim clamábant alter ad álterum:	Two seraphs cry out one after another:
Sanctus, Sanctus, Sanctus Dóminus, Deus Sabaoth	Holy, Holy, Holy Lord, God of Hosts
Plena est omnis terra glória eius.	All the earth is full of his glory.

We also came together in the evening with the rest of the choir to sing Evensong. I think we sang exceptionally well but only seven or so people came to hear it. We sang Stainer's Hail, Gladdening Light as usual, as well as Phillip Moore's third service for the Magnificat and Nunc Dimittis. For the preces and responses, we used Jack Oades' lovely setting. The anthem was John Goss' O Saviour of the World:

O Saviour of the world,

who by thy Cross and precious Blood

hast redeemed us:

Save us, and help us,

we humbly beseech thee, O Lord.

Amen.

I'm still annoyed by the anticipation of the feast day, but I'll never get my way here.

Today we had our regular PhD monitoring event, where all students and faculty in the Foundations cluster go to a remote location for a day, listen to some talks, and hold interviews with students where we ensure they're well supported. We went, as with last time, to the Cuppacumbalong Homestead for this event.

This time the schedule felt quite relaxed and I had a nice time, although I was still suffering from jetlag. My student Kai Phan said she had a better time this time around, which makes me glad.

Salus pópuli ego sum, dicit Dóminus: de quacúmque tribulatióne clamáverint ad me, exáudiam eos: et ero illórum Dóminus in perpétuum.

Eúntes, docéte omnes gentes, baptizántes eos, et docéntes eos serváre ómnia quæcúmque mandávi vobis, dicit Dóminus.

Today I returned to my usual All Saints Ainslie in the morning where we sang Mozart's Ave Verum Corpus under my (metaphorical) baton:

Ave verum corpus natum de María Vírgine;	Hail, true body, born of the Virgin Mary;
Vere passum, immolátum in cruce pro hómine;	True suffering, sacrificed on the cross for Man;
Cuius latus perforátum unda fluxit et sánguine	From whose pierced side flowed waves of blood,
Esto nobis prægustátum in mortis examine.	Be for us a foretaste in death's trial.

I'm still annoyed by the anticipation of the feast day, but I don't think the rector is movable on this subject.

We had a celebration of Gordon Plotkin's eightieth birthday today, featuring many interesting talks. It's hard not to run into Gordon's work if you do anything involving semantics or concurrency or programming languages. My favourite talk of the day was probably my friend Ningning Xie's talk, but I also enjoyed Rob van Glabbeek's talk on his Justness work.

My only major Gordon anecdote is that he was on my interview panel when I interviewed for the job at the University of Edinburgh, and I was astounded to realise that not only was he still alive, but also he somehow didn't appear much older than any of the famous pictures of him.

So, congratulations and happy birthday to the timeless Gordon Plotkin, a huge contributor to our field and an intellectual hero to many of us.

We had a celebration of 40 years since the foundation of the Laboratory for Foundations of Computer Science (LFCS) by Robin Milner, Rod Burstall and Gordon Plotkin today. This was the institute that I was (and in some sense, remain) part of at the University of Edinburgh. I don't have much time for navel-gazing, and sadly most of the technical talks were either well outside my area, a demonstration of how brain-poisoned by LLMs my former Edinburgh colleagues have become, or both. I didn't really get much out of the day.

I am still glad to be here in Edinburgh for this week, though. It's great to catch up with some old friends.

While his birthday was back in April, to fit with Plotkin 80 and LFCS 40, we had a birthday event for Philip Wadler today, celebrating his 70th year.

I really loved Conor's talk on dependent session types, which was inspired by a question from Phil ten years earlier at his 60th birthday event. Her proposed design resembles Peter Hancock's interaction structures quite a bit. Very nice work.

I also gave my talk, which I peppered with many anecdotes about meeting Phil. I got a lot of interest about potentially using Holbert-ng, including from Marcelo Fiore among others. Very exciting stuff!

There was a big movement of "community singing" in the UK during the 1920s (mostly pushed by tory rags). They commissioned Novello and similar music publishers to make score compilations to support community sing-alongs. Today while charity shop perusing, I managed to get the Daily Express compilation (edited by John Goss!) and the News Chronicle compilation, and had a read through. Lots of scottish airs, some hymns and carols, a few american spirituals and folk songs, sea shanties and some British patriotic songs. Interesting charity shop find!

The expanded version of our 2024 paper has finally been published in the journal Information and Computation. This paper includes some of the work that lays the foundation for what I'm now doing with Kai Phan.

Da pacem Dómine, sustinéntibus te, ut prophétæ tui fidéles inveniántur: exáudi preces servi tui, et plebis tuæ Israel.

I sang again at St. Michael and all Saints in the morning where we sang Palestrina's Missa Brevis and Wesley's Wash me throughly:

Wash me throughly from my wickedness

And forgive me all my sin

For I acknowledge my faults

And my sin is ever before me

I also joined the choir at Old St. Paul's once again for Evensong and Benediction. We sang canticles by Harold Darke (both Magnificat and Nunc Dimittis), and an anthem by our own John Kitchen: Stand, Holy Cross, a setting of a text by Gordon Graham (link is to the livestream of the service):

Stand, Holy Cross, between my God and me

And cast a shadow where my heart can hide

Its frail mortality

From his perspicuous light.

The Cross's shade supplies my sin's disguise.

My soul protected, I can turn my eyes;

And now the Father’s light allows me view:

A world, my world, made new.

Then as horizons widen to a farther shore

And light on light enlightens more and more,

This larger vision brings a deeper peace

And sin and sorrow cease.

Stand, Holy Cross, between my God and me.

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.

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.

As I have previously mentioned, I'm on the PC of POPL this year. There were an unprecedented number of submissions (>600), which meant that even with reserve reviewers, each PC member ended up with 14 papers to review. Seeing as POPL papers are typically dense with a fair bit of maths, this is an extreme amount of work.

My workload was exacerbated by the fact that the Toronto paper matching system used by POPL seemed to produce ranks worse than random, so even before being assigned reviews I had to examine (at least the titles of) every submission to the conference to figure out what to bid on.

I don't think we want our PL and FM conferences to end up like AI conferences, with enormous PCs and an even higher volume of papers. I don't want our research to turn into a paper mill where we throw papers over the wall that even the reviewers barely read, let alone anyone else (at best, a disgusting AI summary might be all that is left of our papers for human consumption). But if things keep progressing this way, that's exactly where we'll end up — the volume of papers even in this iteration of POPL is such that I'm having to take shortcuts just to get the reviews done in time.

Normally, my policy is to write a review, wait a day (while not reading anything else), and then submit it, because often I will keep thinking about the paper while I go about my day. This PC membership has made that impossible.

Signum magnum appáruit in cælo: múlier amícta sole, et luna sub pédibus, et in cápite eius in coróna stellárum duodécim.

Gaudeámus omnes in Dómino, diem festum celebrántes sub honóre Maríaæ Vírginis: de cuius assumptióne gaudent Angeli, et colláudant Fílium Dei.

Our director was back from his trip today, so I returned to my deputy role at All Saints Ainslie. Today was a transferred Marian feast which ought to be called "The Assumption of the Blessed Virgin Mary" but due to our protestant-friendly lectionary it's watered down to a feast of "Mary the Mother". While I didn't direct it, I selected the anthem for this week, Stravinsky's Ave Maria:

Ave María, gratia plena, Dóminus tecum.	Hail Mary, full of grace, the Lord is with thee.
Benedícta tu in muliéribus et benedíctus fructus ventris tui, Jesus.	Blessed art thou among women, and blessed is the fruit of your womb, Jesus.
Sancta María, mater Dei, ora pro nobis peccatóribus,	Holy Mary, mother of God, pray for us sinners,
Nunc et in hora mortis nostræ. Amen.	Now and at the hour of our death. Amen.

In exchange for subjecting the congregation to a more unusual setting, I sang Schubert's Ave Maria (in Latin, to the same lyrics) at the end of the service.

We also had a choir management meeting yesterday to set priorities for the coming few months. Nothing firm to announce yet, but we might be bringing some new people into our team, which is very exciting.

I know I'm a bit of a broken record with the anti-LLM posting, but I recently read this excellent article from Katherine Rundell in the Guardian that was not only extremely compelling but also strangely gave me a bit of hope, or at least a call to action.

I talk a great deal about reading for pleasure; I’ve written elsewhere about the necessity of pleasure in the classroom, and why it is not an optional extra but the hallmark of true education. We must find ways to show children that reading gives you access to an inexhaustible source of delight. But I worry, too, that we are limiting the meaning of the word pleasure. Learning is a strange and discomfiting experience; it’s a struggle and a frustration, and epiphanies are rare. It is not always pleasure in its easiest sense.

So I think we also need to talk to young people about reading to outrun and outfight injustice. Reading to get faster, swifter and tougher; to develop powers of scrutiny and criticism and huge creative imagination. Reading human work to insist that we are human. Reading for liberation and emancipation; reading for intellectual freedom, and to have the strength to fight in the arenas of the mind, because when we let a computer think for us, we put a gun to the head of civilisation.

There are dark days ahead. If we are to fight against those with untold financial wealth, we will need untold intellectual wealth. We will need tough-minded people; people with stamina, a huge range of knowledge, and an ability to see wide and far enough to understand in real time what is being done to us. Reading for pleasure and delight are vital – but alongside that and even more urgently: reading for power.

Somehow I missed it that I got an award for my supervision last year. It slipped my mind completely until I got this certificate in my inbox:

Looking at the list of awardees, it seems any supervisor who was nominated was awarded such a commendation (except for the first-place winners). Thank you to whichever of my students nominated me!

Tibi dixit cor meum, quæsívi vultum tuum, vultum tuum Dómine requíram: ne avértas fáciem tuam a me.

I was once again the director of our choir at All Saints Ainslie, on a cold and wet Sunday with few choristers and few parishioners, even though it was a transferred feast. We sang Stopford's Do not be afraid, a poem by Gerard Markland based on the words of Isaiah:

Do not be afraid, for I have redeemed you.

I have called you by your name;

you are mine.

When you walk through the waters,

I'll be with you;

you will never sink beneath the waves.

When the fire is burning all around you,

you will never be consumed by the flames.

When the fear of loneliness is looming,

then remember I am at your side.

When you dwell in the exile of a stranger,

remember you are precious in my eyes.

You are mine, O my child,

I am your Father,

and I love you with a perfect love.

Do not be afraid, for I have redeemed you.

I have called you by your name;

you are mine.

There's something weird going on, because we celebrated the Transfiguration already on Quinquagesima Sunday, and last year they made no special observance of the feast of the Transfiguration. The transferring of feasts is such a mess! I'm liking Oliver Brewer-Lennon's policy of never transferring anything and celebrating feasts on the day more and more.

As part of Xin Lu's project we needed to come up with a version of CCS that supports explicit termination in the style of ACP. There is a paper by Luca Aceto and Matthew Hennessy which introduces a termination predicate, but they require that a nondeterministic choice P + Q is judged terminating (written P + Q \checkmark ) only when both P \checkmark and Q \checkmark . In other words, a process is only terminating if it has no choice but to terminate.

In our case, we want a judgement for possible termination, not guaranteed termination. So we had to come up with our own notions. We've formalised this in Isabelle, but what follows is the same but presented as Forester notes. Eventually, these notes may become part of another research notebook or even lecture notes.

You know the drill by now. Another article I read about the damage LLMs are doing to our intellectual pursuits. This is a deeply personal reflection from a mathematician, Kirwin Hampshire: The Dark Night of Mathematics.

There is nothing I can do. There may be nothing you can do. I have no prescriptions, policy recommendations, or coherent call to action. I just want to be honest and open about my emotional and spiritual response. I want to feel seen. I want folks like me to feel seen. I need the architects of our new mathematical paradigm to look me in the eye and acknowledge our shared humanity and soul before they deliver the coup de grâce. I need, most of all, for us to understand what we are really doing.

Deus in adiutórium meum inténde: Dómine ad adiuvándum me festína: confundántur et revereántur inimíci mei, qui quærunt ánimam meam.

I was once again the director of our choir at All Saints Ainslie, for the special Missing Persons Sunday today, with representatives from the Australian Federal Police present to offer special reflections and awareness about those who are missing in our territory and support their loved ones, many of whom were in attendance. We performed Rachmaninoff's Bogoroditse Devo:

Богородице Дево, радуйся,	Rejoice, virgin mother of God,
Благодатная Марие, Господь с тобою.	Mary, full of grace, the Lord is with you.
Благословена ты в женах,	Blessed are you among women,
и благословен плод чрева твоего,	and blessed is the fruit of your womb,
яко Спаса родила еси душ наших.	for you have borne the Saviour of our souls.

I've begun adding more to the material in my research notes on linear temporal properties. We've now covered the "top diamond" described in my note about my work with Kai Phan. Hope to add more this week!

Deus in loco sancto suo: Deus, qui inhabitáre facit unánimes in domo: ipse dabit virtútem et fortitúdinem plebi suæ.

I was once again the director of our choir at All Saints Ainslie, where we sang two anthems to a packed house: there were fourteen confirmees, and the bishop (and primate of Australia) came to induct them into the church. Our choir sang a favourite of mine, Lloyd's View Me, Lord, a lovely poem from Thomas Campion:

View me, Lord, a work of thine.

Shall I then lie drown'd in night?

Might thy grace in me but shine,

I should seem made all of light.

Cleanse me, Lord, that I may kneel

At thine altar, pure and white.

They that once thy mercies feel

gaze no more on Earth's delight.

Worldly joys, like shadows, fade

When the heav'nly light appears;

But the cov'nants thou hast made,

Endless, know not days nor years.

In thy word, Lord, is my trust;

To thy mercies fast I fly.

Though I am but clay and dust,

Yet thy grace can lift me high.

As well as Tallis' If ye love me, which, at least in my edition, was in the exact same key.

If ye love me, keep my commandments.

And I will pray the Father,

And He shall give you another comforter:

That He may bide with you forever, e'en the Spirit of Truth.

I also directed us for evensong, where we sang a mostly plainchant evensong, along with Stainer's Hail, Gladdening Light as usual, plus Vaughan Williams' The Call as an anthem (with solo verse sung by yours truly), from his settings of George Herbert poems, the Five Mystical Songs.

Come, my Way, my Truth, my Life;

Such a Way as gives us breath,

Such a Truth as ends all strife,

Such a Life as killeth death.

Come, my Light, my Feast, my Strength;

Such a Light as shows a Feast,

Such a Feast as mends in length,

Such a Strength as makes his guest.

Come, my Joy, my Love, my Heart;

Such a Joy as none can move,

Such a Love as none can part,

Such a Heart as joys in love.

We got back our student experience evaluations for our teaching in semester one. I'm pleased to report that I managed to bring Structured Programming from being one of the most unpopular courses in the university to one of the more liked, with 83% of respondents giving the thumbs up to the course and 95% to my teaching specifically, and no negative ratings. In particular, I was pleased that 100% of respondents indicated that I "treat students with respect".

I particularly was glad to read this comment:

Liam is an excellent communicator, educator, and convenor. He consistently takes time after his lectures to answer student questions and support them with the course content. His live coding is impressive, and he battles through IT issues without losing it, which is impressive in it's own right. His lectures are engaging and for those who attend I believe it to be an excellent learning experience. By doing crowd informed live coding he engages each of us in the process of solving the problem the first time, while he demonstrates the new concept. This leaves you feeling like you CAN do it. That the new concept isn't so alien, because you saw all the steps to build it. This is a huge confidence booster going into the lab, as now this is the second time you are trying to implement the concept, alone this time. He was quick to address student concerns on the forum and consistently asking students for feedback and suggested improvements. He showed genuine concern in the students that were struggling in the midsemester exams and adapted the course for their expressed needs. He is an excellent educator and I hope to take more of his classes in the future.

The ANU Logic Summer School is back again this year, and I will once again teach my ITP course. The timetable is not yet finalised, but I will likely not have to teach it all over two days as I did last year, which is a relief. It will likely run in the early days of December.

If you or your students have an interest in logic or verification, please consider sending your students! We also have some limited scholarships available.

Dóminus fortitúdo plebis suæ, et protéctor salutárium Christi sui est: salvum fac pópulum tuum, Domine, et bénedic hereditáti tuæ, et rege eos usque in sæculum.

Today I didn't attend my usual All Saints Ainslie as I was visiting Sydney, so I attended Christ Church St. Laurence instead. The choir was mens voices who sang the gregorian mass setting cum jubilo as well as The Call by Ralph Vaughan Williams, a setting of a poem by Herbert:

Come, my Way, my Truth, my Life:

Such a Way, as gives us breath:

Such a Truth, as ends all strife:

Such a Life, as killeth death.

Come, My Light, my Feast, my Strength:

Such a Light, as shows a feast:

Such a Feast, as mends in length:

Such a Strength, as makes his guest.

Come, my Joy, my Love, my Heart:

Such a Joy, as none can move:

Such a Love, as none can part:

Such a Heart, as joys in love.

It was a very restorative service, even for my (Buddhist) in-laws. I believe that my usual choir performed "Thee we adore" by T. Frederick H. Candlyn in my absence, an arrangement of adoro te devote.

Omnes gentes, pláudite mánibus, iubiláte Deo in voce exsultatiónis. Quóniam Dóminus excélsus, terríbilis: Rex mangus super omnem terram.

Today we were in light numbers at All Saints Ainslie but still pulled off a solid performance of How's Day by Day

Day by day, dear Lord,

of thee three things I pray;

to see thee more clearly,

to love thee more dearly,

to follow thee more nearly,

day by day.

This service included the baptism of many children all from the same family, so it was a rather special service in that respect. Later in the month we will have a confirmation service with fourteen (14!) confirmees, which is a promising sign for the health of the parish.

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.

As our director has started a UK tour with his secular singing ensemble, I have taken on the job of interim director at All Saints Ainslie, where we sang today Howell's My eyes for beauty pine:

My eyes for beauty pine,

My soul for Goddës grace:

No other care nor hope is mine,

To heaven I turn my face.

One splendour thence is shed

From all the stars above :

'Tis named when God's name is said,

'Tis Love, 'tis heavenly Love.

And every gentle heart,

That burns with true desire,

Is lit from eyes that mirror part

Of that celestial fire.

I think they transferred the feast of St. James to today rather than to the following Sunday (which is closer), because they want to focus the service next week on confirmations with the Bishop.

I quite enjoyed this article by Glyph. It pins down quite well what makes me somewhat concerned about the "autoformalisation" hype in the mathematics community. Mathematics has, up to now, considered all communication (beyond obvious cranks) to have some degree of good faith. The use of LLMs in mathematics have the potential to turn all of mathematics into an adversarial "find the flaw" game. I don't want to participate in an intellectual field like that.

I know I'm becoming a broken record in collecting anti-LLM articles and talking points, but it really is an article of faith for me.

My partner will be studying at the University of Canberra so I went on a little tour of their campus with her. There seems to be a mob of Kangaroos (is that the right collective noun?) that lives on the campus there. They are the grey Kangaroos that can be seen elsewhere in Canberra, but that doesn't stop the males from being intimidating both in size and musculature. I was also struck by how small the campus is in terms of buildings for the amount of space it occupies. A much smaller scale operation than the Australian National University seems to be.

NUNC scio vere, quia misit Dóminus Angelum suum: et erípuit me de manu Heródis, et de omni expectatióne plebis Iudæórum.

This morning at All Saints Ainslie I was the cantor for the morning mass, and with a soprano Cindy Chen (who was playing the organ for the other parts of the mass), we sang a 13th century English "gymel" piece, arranged by yours truly (I don't have a recording sadly):

Jesu Cristes milde moder stud biheld hire sone o rofe that he was ipined on.	Jesus Christ's mild mother stood and beheld her son on the rood that he was pinned on.
The son heng, the moder stud and biheld hire childes blud wu it of hise wundes ran.	The son hanged, the mother stood, and beheld her child's blood as it from his wounds ran.
Neue blisse he us broute that mankin so dere boute, and for us gaf is dere lif.	New blessings he to us brought, for mankind so dearly bought, and for us gave his dear life.
Glade and blithe thu us make, for thi swete sones sake, edi maiden blisful wif.	Glad and blythe thou us make, for thy sweet son's sake, noble maiden, blessed wife.
Quen of evene for thi blisse lithe al hure sorinesse and went hur yvel al into qud.	Queen of Heaven, for thy blessedness lightens all our sorrows and turns our evil all into good.
Bring hus, moder, to thi sonne, mak hus ever with him wone that hus boute wit this blud.	Bring us, mother, to thy son. Make us ever with him one, that he bought with this blood.
Amen.	Amen.

I returned to the church in the evening for Evensong. We sang Stainer's Hail, Gladdening Light as usual, as well as Phillip Moore's third service for the Magnificat and Nunc Dimittis. For anthem, we sang the first of Parry's Songs of Farewell, which we had previously performed at our recent concert: My soul there is a country

My soul, there is a country

Far beyond the stars,

Where stands a wingèd sentry

All skilful in the wars:

There, above noise and danger,

Sweet Peace sits crown'd with smiles,

And One born in a manger

Commands the beauteous files.

He is thy gracious Friend,

And—O my soul, awake!—

Did in pure love descend

To die here for thy sake.

If thou canst get but thither,

There grows the flower of Peace,

The Rose that cannot wither,

Thy fortress, and thy ease.

Leave then thy foolish ranges;

For none can thee secure

But One who never changes—

Thy God, thy life, thy cure.

I finished and marked the final exam for Structured Programming last week. I enjoyed teaching this course but I am very glad it's over. Perhaps surprisingly, considering the catastrophic results from my earlier exam, but the students in general did alright. Perhaps the poor performance shocked them into action somewhat and they practiced more. I also think I made the final exam a little gentler than the other assessments.

One thing that I regret doing, and will change in future iterations, is that the homework assignments (which I no longer trust as summative assessment, as they are solvable by LLM) did not have fixed due dates, but instead only recommended due dates before the exam/test for which they served as practice. The actual final due date was just at the end of semester, before the final exam I just marked. The result was, predictably in hindsight, that students didn't do the homework until the last minute, depriving them of the necessary programming practice before the midsession tests. We won't repeat this mistake.

Kai Phan has been building on her already very impressive result to produce a very nice picture of the monitorability landscape. I will present a brief summary of her results here, but eventually they will be incorporated into my research notebook on linear-time temporal properties. Mostly, our results concern the space of program properties — sets of program behaviours.

The classes of safety and guarantee above are the familiar closed and open sets respectively in the topology of program behaviours. In the above diagram, decision properties are the clopen sets — those sets that are both Safety properties and Guarantee properties, and obligation properties are, following Amir Pnueli, any boolean combination of closed or open sets.

Kai's original result was to show that all Bauer monitorable properties — that is, all properties for which a monitor can always potentially give an answer — cannot be distinguished from an obligation property by any monitor observing finite prefixes. What she has now done is prove that Bauer monitorable properties are exactly those properties that approximate an obligation property in this way. This led us to re-christen Bauer monitorability as the class of quasi-obligation properties. In a similar way, she has also identified the classes of quasi-safety and quasi-guarantee, which cannot be monitorably distinguished from safety and guarantee properties respectively, and proved that quasi-obligation properties are exactly those that are made up of boolean combinations of these.

At the bottom of the prism, we have another set of classes. What is commonly called weak monitorability sits at the very bottom — those properties for which there is at least one finite prefix that causes a monitor to give a definitive answer. We also have good monitorability and bad monitorability, which are those properties with at least one good or bad prefix respectively. It is easy to see that weak monitorability is the union of these classes. (Taking boolean combinations, as in the higher levels of the cube, leads to a trivial class containing all properties).

Kai has also now defined CTL characterisations for all of these lower classes, expressed as formulae over monitor trees, which we define reminiscent of Ghani, Hancock and Pattinson's stream processors. She then showed that the CTL formulae for all of the middle layer classes of the prism are obtained by wrapping the corresponding formula for the class below with \mathbf {AG}. For example, weak monitorability is defined as \mathbf {EF}\ (\mathit {yes} \lor \mathit {no}), and quasi-obligation is just \mathbf {AG}\ \mathbf {EF}\ (\mathit {yes} \lor \mathit {no}). Because of the aforementioned indistinguishability result (and because indistinguishable properties have indentical monitors), it's not possible to write CTL formulae for the top level of the prism, except for Decision properties (clopen sets) which correspond exactly to those monitors described by inductive trees — where all paths eventually terminate with an answer.

We're aiming to get this into ESOP or FoSSaCS this year. Hoping for the best! I think this is great work.

Dóminus illuminátio mea, et salus mea, quem timébo? Dóminus defénsor vitæ meæ, a quo trepidábo? Qui tríbulant me inimíci mei, infirmáti sunt, et cecidérunt.

Si iniquitátes observáveris Dómine, Dómine quis sustinébit? Quia apud te propitiátio est, Deus Israel.

Today at All Saints Ainslie we sang Palestrina's well-known Sicut Cervus:

Sicut cervus desíderat ad fontes aquárum:	Like as the hart desireth the waterbrooks:
ita desíderat ánima mea ad te, Deus.	So longeth my soul after thee, O God.

We didn't make any observation of the Sacred Heart, but that's not entirely unexpected for an Anglican parish, even a relatively spikey one.

Exáudi Dómine vocem meam, qua clamávi ad te: adiútor meus esto, ne derelínquas me neque despícias me, Deus salutáris meus.

Today at All Saints Ainslie we were in very reduced numbers — 1 to a part — but we sang Bob Chilcott's God so loved the world wonderfully!

God so loved the world

That he gave his only-begotten son

That whoso believeth in him should not perish

But have everlasting life.

Special thanks to Cindy Chen, our soprano soloist, and Mary-Anne Neilsen for stepping in and playing the organ at the last minute.

This week I attended (along with many others from ANU including Peter Höfner, Ali Nosherwan Hamed, Xin Lu, Kai Phan and Carlo Zancanaro) the yearly meeting of Formal Methods researchers in Australia at the University of Queensland. It was good to hear from colleagues again, and I was very impressed by the size of the group.

Peter Höfner also presented some of the initial thoughts and work around Yi Yao's PhD topic, and it was good to help clarify our thinking there. I think I will encourage all of my students not just to attend, but also to speak next year.

We encountered a kookaburra at breakfast that seemed determined to steal people's sausages (swooping right in front of them). This kookaburra seems to have absolutely no fear of humans, so I was able to get very close to take a picture. Eventually we saw it smashing a piece of bread against the table to "kill" it, as they do to lizards and snakes in more natural contexts.

This is a special edition of Church Music Corner where I share the programme for the second church choir concert of 2026, To the Soul's Quiet Harbour, continuing in the funerial theme established by our first concert. The student musicians from Burgmann Anglican School joined us at All Saints Ainslie to perform an afternoon of chamber music to a fairly full house. We sang pretty well despite being lopsided in numbers (I was the only tenor.)

The main works performed by the choir (interspersed by instrumental performances from Burgmann) were the first four of Parry's Songs of Farewell: My soul, there is a country, then I know my soul hath power, then Never weatherbeaten sail and There is an old belief. The last item of the concert was O How Amiable by Ralph Vaughan Williams, which we sung with pipe organ, choir, and instruments.

I think the concert went rather well. Thanks to all who put the effort in to make it possible, and to everyone that attended!

Respice in me, et miserére mei, Dómine: quóniam únicus et pauper sum ego: vide humilitátem meam, et labórem meum: et dimíte ómnia peccáta mea, Deus meus.

Cibávit eos ex ádipe fruménti, allelúia, et de petra, melle saturávit eos, allelúia, allelúia, allelúia.

Today at All Saints Ainslie we were in few numbers after our concert yesterday but we still managed to sing Tallis' Verily, verily I say unto you (link to my own recording I made last year):

Verily, verily, I say unto you:

Except ye eat the flesh of the Son of Man

and drink his blood,

ye have no life in you.

Whoso eateth my flesh,

And drinketh my blood,

Hath eternal life.

For my flesh is meat indeed,

and my blood is drink indeed,

He that eateth my flesh and drinketh my blood

Dwelleth in me, and I in him.

We didn't make any observation of the feast of Corpus Christi which I'm a bit unhappy about (but that's why we have at least got that Tallis anthem programmed).

I have been reading and digesting in pieces the new encyclical from Pope Leo XIV, Magnifica Humanitas. While in some places I feel it doesn't quite go far enough, and the Vatican has troubling connections to Anthropic, I think that the content of the encylclical itself is very good.

One of the things that I always believed even while I was an atheist was the infinite worth of human beings. This aspect that underpins much of Catholic social teaching has always been one of the things I agree with, and part of why I find artificial simulacra of human connection, human relationships, human personality or human creativity so offputting and spiritually uncomfortable.

The Pope's new writing really rams home this foundation of Catholic social teaching with reference to AI. It's not really an encyclical about AI, but rather using the issue of AI to introduce folks to this teaching of the church.

There is also the more profound and important level of ontological dignity. This is the dignity that belongs to every human being simply by virtue of existing, of having been willed, created and loved by God. No sin, failure, humiliation or exclusion can diminish the profound value of a human life that God has willed and called into being.

Another aspect of Christianity that I really like is that it embraces love as a relation. We must express and receive love for one another to experience God. Without acknowledging others, embracing and accepting others, and loving others, we cannot be any nearer to God. Simply meditating or looking within oneself may clarify one's thoughts but it cannot bring us to love. Understanding and accepting human life, in all its diversity, including all its joys and difficulties, as something to be loved and experienced rather than suppressed or even transcended is a part of the Christian view, and something that I really appreciate. It seems like Leo agrees:

Even when limitations are experienced as inner suffering, human wisdom teaches us not to deny or suppress it, but to integrate it. To eliminate suffering entirely would mean, in the end, extinguishing love and desire as well. Those who love and desire cannot avoid passing through trial and suffering; and over the years, we carry within us lessons that leave their mark like scars, the memories of a journey shaped by freedom and failure, dreams and disappointments. It is only thanks to the interplay of these elements that the wonders of the soul occur within us, allowing us to sense the richness of our humanity. To renounce this adventure, both tragic and splendid, in the name of a presumed transcendence of all limits, could mean many things, but it would no longer be human.

He touches on many more topics, and I strongly recommend folks take the time to read it. I'll finish by just quoting one passage that seems to be sending a lot of LLM-poisoned idiots on twitter into a tizzy, despite being obviously correct:

So-called artificial intelligences do not undergo experiences, do not possess a body, do not feel joy or pain, do not mature through relationships and do not know from within what love, work, friendship or responsibility mean. Nor do they have a moral conscience, since they do not judge good and evil, grasp the ultimate meaning of situations, or bear responsibility for consequences. They may imitate language, behavior and analytical skills, or even simulate empathy and understanding, but they do not understand what they produce, for they lack the affective, relational and spiritual perspective through which human beings grow in wisdom. Even when these tools are described as capable of “learning,” their way of doing so is different from that of a human person. It is not the experience of those who allow themselves to be shaped by life and grow over time through choices, mistakes, forgiveness and fidelity. Rather, it is a form of statistical adaptation based on data and feedback, which can be very effective, but does not imply inner growth.

Benedícta sit sancta Trínitas, atque indivísa Unitas: confitébimur ei, quia fecit nobíscum misericórdiam suam.

Caritas Dei diffúsa est in córdibus nostris, alleluia: per inhabitántem Spíritum eius in nobis, allelúia, allelúia.

Today at All Saints Ainslie our choir absolutely nailed the performance of William Byrd's beautiful and heartbreaking setting of Ave Verum Corpus

Ave verum corpus natum de María Vírgine,	Hail, true body, born of the Virgin Mary,
Vere passum immolátum in cruce pro hómine,	True suffering, sacrificed on the cross for Man,
Cuius latus perforátum unda fluxit sánguine,	From whose pierced side flowed waves of blood,
Esto nobis prægustátum in mortis exámine.	Be for us a foretaste in death's trial.
O dulcis, O pie, O Iesu fili Maríæ,	O sweet! O blessed! O Jesus, son of Mary,
Miserére mei, miserére mei, miserére mei.	Have mercy on me, have mercy on me, have mercy on me.

This Thursday is Corpus Christi, but I'm flying to Brisbane so I won't be able to make any observances this year, and Ainslie doesn't do anything in any case.

Also, this Saturday our choir is doing a concert with instrumentalists from the Burgmann Anglican School in Gungahlin.

The instrumentalists will perform a variety of pieces interspersing our performance of (the first four of) Parry's Songs of Farewell, finishing with us all performing some Ralph Vaughan Williams.

Do come down to All Saints Ainslie and support our music fund!

Spíritus Dómini replévit orbem terrárum, allelúia: et hoc quod cóntinet ómnia, sciéntiam habet vocis, allelúia, allelúia, allelúia.

Today at All Saints Ainslie the Choir was on for Evensong so our director Alasdair handled the music in the morning with our guest accompanist, Zac Hamilton-Russell. He sang Dering's Duo Seraphim with Zac's partner (whose name I now can't recall, sorry!) who has a lovely soprano voice! I stayed at the church all day reorganising our music, and because Alasdair and Zac had a recital until the late afternoon, I rehearsed and conducted the choir for Evensong. We sang Stainer's Hail, Gladdening Light as usual, as well as Phillip Moore's third service for the Magnificat and Nunc Dimittis. For anthem, we sang Hurford's Litany to the Holy Spirit:

In the hour of my distress,

When temptations me oppress,

And when I my sins confess,

Sweet Spirit, comfort me!

When I lie within my bed,

Sick in heart and sick in head,

And with doubts discomforted,

Sweet Spirit, comfort me!

When the house doth sigh and weep,

And the world is drown'd in sleep,

Yet mine eyes the watch do keep,

Sweet Spirit, comfort me!

It was a bit stressful as I wasn't planning to direct our choir but I did okay I think.

Also, the sermon by Oliver Brewer-Lennon from St. Michael and All Saints was brilliant as usual. He's the only priest whose (usually quite brief!) homilies I actually seek out and listen to, sometimes multiple times. Because my partner was curious, I translated it into Korean.

Our concert Radiant Dawn got a nice review in the local Canberra paper City News. You can read it here.

Mostly the review recapitulates the programme, but I'm glad that we "sung with emotional intensity and joyful celebration."

I do agree with the one commenter though:

Incredibly disappointing to see the program notes were written with AI.

I do know how this happened (things were prepared very much at the last minute), but I don't think it's an excuse. I'll have a word with Coro next time we run a concert to make sure this doesn't happen again.

I'm happy to report that the small grant I applied for with Charles Martin was successful. We will get a few thousand dollars to set up a teaching activity where students will program with punch cards again.

The key to this approach will be having only one card reading/program executing machine for all students, who must then book computer time just like in the old days of batch processing. I also thing there's something important about the physicality of punching holes in cards that students might appreciate. It's also LLM-proof programming, so there's that.

Today we had a cleaning bee at All Saints Ainslie where we cleaned up the organ loft and choir section of the church. It's a much nicer space to sing in now!

The choir has accumulated several musical treasures, one of which is an old but still decent edition of the original Church Anthem Book from Oxford, which I was allowed to take home with me. This impression is from 1954, but it was first printed in 1933. The successor book, the New Church Anthem Book, includes many of the same anthems but there are several (now added to my Music Index) anthems that are new to my collection.

Viri Galilæi, quid admirámini aspiciéntes in cælum? Allelúia: quemádmodum vidístis eum ascendéntem in cælum, ita véniet, allelúia, allelúia, allelúia.

Today at All Saints Ainslie we sang very well for Isom's King of all ages. I'm a bit disappointed that, unlike last year, we transferred the feast to the Sunday, though:

King of all Ages, throned on high,

Yet saviour too of those with faith,

Death at your onslaught died in fear,

And grace triumphant rules supreme.

Risen from death, the heav'nly Christ,

Receives from God the Father's hand,

Power over all created things,

A gift he could not know on Earth.

Then at your coming on the clouds,

With shining strength to be our judge,

Cancel the debt we owe you still,

Give back the glory we have lost.

Glory to you, O Christ our Lord,

Exalted far beyond our sight,

Reigning and forevermore,

with Father and with Paraclete.

I made a post on Mastodon that seemingly did numbers.

I don't know who needs to read this, but: there's value in doing things slowly, in your own way. Trying to maximise efficiency in your life is a fool's errand, and will just hurt you. Take the longer route with the nicer scenery. Write that email by hand instead of asking a bot to do it. Spend some time to read and not just skim. Take your time and cook a nice meal for yourself. Pursue little hobbies, even if you're not good at them. Don't compare yourself to others, don't focus on improving. Just enjoy every activity for itself. Don't let the world convince you that you always have to be optimising yourself. Just be sub-optimal and happy!

The reason I wrote this is because I read a thread on X (the everything app) which made my blood boil somewhat. Academics were saying that the reason they train students rather than just do research themselves with dreaded bots doing all the legwork is that there's value in the apprenticeship, in training a person. To me, that's a bad argument because it presupposes both that we should be prioritising efficiency above all else (definitely disagree) and that working with AI is more efficient in the long run than working with a student (also disagree but falsifiable).

I was devastated earlier this week when I marked the midsemester test for the first year course I'm teaching at the ANU. Less than one in five students passed the test, with more than half of submissions showing compile errors when running automatic tests on their code (this is for the second programming course in our programme, mind). My tutors completed the exam (100% correctly) in 25 minutes, and I gave my students 90 minutes.

I am fairly confident that this result is not a result of some deep failing on my part — I've taught first year students before with much better results — so I did a little digging to see how much students are engaging with my course. The results were not encouraging. More than half of students had not even started Homework 1, which came out at the beginning of semester (ten weeks ago), and fewer than one in five students had started Homework 2, which was directly intended to prepare them for the very test they failed. I hear reports from my tutors that students have begun education-defeating practices like copying a lab exercise into ChatGPT without even reading it.

This is all a symptom of the broader engagement crisis in teaching and an overall worrying decline in conscientiousness that is deeply troubling and bodes poorly for the future. Lecture attendance is extremely low. Usually I get no more than twenty students (out of about one hundred and twenty) in my lecture theatre. Frustratingly, it's precisely those students — the students I can actually reach — that I'm not worried about. When bad results come out like this, a lot of the relatively conscientious but struggling students begin to feel like they should give up and withdraw (and this pressure disproportionally affects under-represented groups such as female students). The rest of the semester has become a delicate morale balancing act where I need to shock students enough to get them to switch their brains on, but avoid demoralising students such that those who have ability but lack confidence are not discouraged.

I've retooled the remainder of the semester. We're going to do only the essentials in terms of more content. The rest will just be drilling exercises to help them gain the basic study skills they should already have by now. I'm so much more depressed and anxious running my course this way. I hope I can teach a 3rd year elective one day and be somewhat relieved of this.

I successfully performed in my first concert with Coro. I think it went very well, and I saw some familiar faces in the audience (including Fabian Mühlböck!). The programme was a very nice (although eclectic) collection of music spanning centuries. Some of my favourites included Lobo's Versa est in luctum, Stravinsky's Ave Maria, the Agnus Dei movements from all of Byrd's Masses, including the Byrd 5, and Morten Lauridsen's O Magnum Mysterium. It was a delight to sing with these talented singers and I'm looking forward to our next concert later in the year!

Vocem iucunditátis annuntiáte, et audiátur, allelúia: nuntiáte usque ad extrémum terræ: liberávit Dóminus pópulum suum, allelúia, allelúia.

Today at All Saints Ainslie I conducted a small group for the Crux Fidelis commonly (but almost certainly wrongly) attributed to John IV of Portugal (I took Neale's translation rather than a more direct one):

Crux fidélis, inter omnes	Faithful Cross, above all other,
Arbor una nóbilis:	One and only noble tree:
Nulla talem silva profert,	None in foliage, none in blossom,
Fronde, flóre, gérmine.	None in fruit thy peer may be.
Dulce lignum, dulci clavo,	Sweetest wood and sweetest iron,
Dulce pondus sústinens.	Sweetest weight is hung on thee.

I'm in a bit of a pickle, although I accept it sounds like an academic "first-world problem": I already have three first year PhD students (Yi, Kai and Xin) that I supervise quite actively. I still have funding for one more international place and I'm currently talking to four additional people who want to do a PhD with me, some of whom are local students so very likely to get funding. The worry is twofold:

1. I'm starting to run out of good topic ideas to help possible students get started on a proposal, and
2. I don't think I'm capable of supervising many more students, at least not in their first year. Once my existing students are further along it might be easier.

I am worried that I might have to start turning good people down — although I don't want to. But I fear that if I accept too many students the outcome will be worse for all of us.

Cantáte Dómino cánticum novum, allelúia: quia mirabília fecit Dóminus, allelúia: ante conspéctum géntium revelávit iustítiam suam, allelúia, allelúia.

Today at All Saints Ainslie we reprised Goss' anthem O Saviour of the World from our concert earlier in the year:

O Saviour of the world,

who by thy Cross and precious Blood

hast redeemed us:

Save us, and help us,

we humbly beseech thee, O Lord.

Amen.

After that I had a rehearsal with Coro for our upcoming concert, Coro Concert: Radiant Dawn. Please buy tickets and come along!

My student Kai Phan was absolutely on fire this week. About five times I threw out a few idle conjectures I had, and within hours she'd come back with a proof or a counterexample. We made more progress in one week than I had thinking about this stuff for months.

It's well known in the world of runtime verification that the class of monitorable properties (by which I mean the definition used by Bauer, where no monitor will get into an "ugly" state where no informative answer is possible) is larger than the set of safety or guarantee properties, or their boolean combinations (called obligation properties or \Delta _2).

What Kai showed recently is that all monitorable properties are indistinguishable by any monitor from an obligation property. This shows that a lot of the monitorability classes we find in the literature are making a distinction from standard sets in \Delta _2 that is only observable at infinity anyway. So the "largeness" of the monitorability classes is illusory, and obligation properties are all you need.

The proof has been mechanised in Isabelle/HOL, and we have a number of other supporting contributions that I think will make a good paper for POPL or LICS. I'm very proud of Kai's progress so far! I think this result will reinforce her plan for her thesis, which is to semantically tackle revocable monitors (i.e. monitors that can change their mind). Seeing as the difference hierarchy is contained at all finite levels in \Delta _2, we should have an easy time justifying restricting to \Delta _2 properties now.

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.

Coro, one of Canberra's leading choral ensembles and two-time Canberra Critics' CIrcle Award recipient, invites audiences to experience Radiant Dawn: From Lamentation to Light, an extraordinary hour of choral music that traces the path from sorrow and supplication to renewal, wonder, and radiant joy.

This thoughtfully curated program - the ensemble's first for 2026 - brings together masterpieces from the Renaissance and the modern era, revealing how composers across centuries have responded to the deepest human emotions with beauty, faith, and hope.

Beginning in stillness and grief with three great sacred works of the Renaissance by Handl, Victoria, and Lobo, these works explore mortality, sorrow, and the search for consolation. Yet from darkness emerges hope. William Byrd’s three exquisite settings of the Agnus Dei — for three, four, and five voices — chart a journey from intimate simplicity to glorious fullness of sound. Interwoven are Igor Stravinsky’s luminous Ave Maria and Claude Le Jeune’s joyful Revecy venir du printemps, suggesting grace, renewal, and the first stirrings of life.

At the centre of the evening, and giving the concert its title, stands James MacMillan’s breathtaking O Radiant Dawn, a contemporary choral masterpiece of glowing sonorities and spiritual intensity.

Celebrating life with energy, intimacy and warmth, the afternoon closes with works by Finzi and Chilcott, followed by Morten Lauridsen’s beloved O Magnum Mysterium.

Radiant Dawn: From Lamentation to Light is a concert of striking contrasts and deep emotional resonance — music that journeys through shadow into brilliance, reminding us of the enduring power of the human spirit.

Misericórdia Dómini plena est terra, allelúia: verbo Dei cæli firmáti sunt, allelúia, allelúia.

Today at All Saints Ainslie I was planning to sing Dering's Duo Seraphim as a duet with our choir director but he was exhausted and unable to come in for the morning mass, so instead I sang some Gregorian chants, specifically the introit for this Sunday in Latin (text above), the Easter Sequence in English using an older translation I remember from St. Mary's Cathedral (text below), and then the introit for last sunday:

Christians to the Paschal victim offer sacrifice and praise.

The sheep are ransomed by the Lamb;

And Christ, the undefiled, hath sinners to his Father reconciled.

Death and life contended, combat strangely ended:

Life's own champion slain, yet lives to reign.

Tell us, Mary, what thou didst see upon the way.

The tomb the living did enclose, I saw Christ's glory as he rose.

The angels attesting, shroud with graveclothes resting.

Christ my hope has risen! He goes before you into Gallilee.

That Christ is truly risen from the dead we know.

Victorious King, thy mercy show. Amen. Alleluia.

After that we had choral evensong for this month, this time directed by our usual director. We sang Stainer's Hail, Gladdening Light as usual, as well as Phillip Moore's third service for the Magnificat and Nunc Dimittis (it's hard to find good recordings). Because it was the day after Anzac Day, we also sang Daley's In Remembrance.

Do not stand at my grave and weep;

I am not there, I do not sleep:

I am a thousand winds that blow,

I am the diamond glint on snow,

I am the sunlight on ripened grain,

I am the gentle morning rain.

And when you wake in the morning's hush,

I am the sweet uplifting rush

Of quiet birds in circled flight.

I am the soft stars that shine at night.

Do not stand at my grave and cry,

I am not there, I did not die.

Today we had our regular PhD monitoring event, where all students and faculty in the Foundations cluster go to a remote location for a day, listen to some talks, and hold interviews with students where we ensure they're well supported. We also try to run some fun activities and get the students socialising with each other. It's always an enjoyable day.

This time we had a fairly packed schedule and many students to get through, so I didn't get any time to play frisbee, although I did take a few nice shots of the landscape around the Cuppacumbalong Homestead where we held our event.

I met a few students who were new to me and had a few stimulating research discussions, and my students Kai Phan, Xin Lu and Yi Yao got to know each other and other students a bit better. The day was quite a success, I think.

Iubiláte Deo omnis terra, allelúia: psalmum dícite nómini eius, allelúia: date glóriam laudi eius, allelúia, allelúia, allelúia.

Today at All Saints Ainslie our director Alasdair was our ad-hoc organist as we sang Mozart's Ave Verum Corpus:

Ave verum corpus natum de María Vírgine;	Hail, true body, born of the Virgin Mary;
Vere passum, immolátum in cruce pro hómine;	True suffering, sacrificed on the cross for Man;
Cuius latus perforátum unda fluxit et sánguine	From whose pierced side flowed waves of blood,
Esto nobis prægustátum in mortis examine.	Be for us a foretaste in death's trial.

After the mass I had my first rehearsal for the upcoming Coro concert. It was very productive. One piece of repertoire that really stuck with me was the Stravinsky Ave Maria, which I'd not heard before.

I have made significant additions to my research notes on Linear-time temporal properties. Now I have all the relevant content from Defining Liveness, and some of the definitions that will appear in the forthcoming journal paper from me and Rayhana Amjad. This paper finally got reviews back, and we have quite a few things to do but I'm confident we'll get there.

My students Mio Wu and Josh Brown have been doing some great work on the next generation of the Holbert proof assistant. In particular, Josh has now implemented a pluggable term structure, allowing various types of terms, each with their own unification methods and structure definitions, to be combined together in judgements. Mio is confident she can generalise his approach to work for higher order terms as well, which is very exciting.

As part of my general desire to stop using anything that feeds the LLM bots, I am gradually beginning to migrate off of GitHub. Fortunately the Holbert-NG crew are also happy to leave GitHub, so we are going to move to tangled for the time being.

I also got the chance to do some programming work myself. Soon we should have a similar proof UI to what the original Holbert has. I think most of the architecture is in place now.

Quasi modo géniti infántes, allelúia: rationábile, sine dolo lac concupíscite, allelúia, allelúia, allelúia

Today at All Saints Ainslie we had small numbers (I was the only tenor) but sang well for Walford Davies' Blessed are the pure in heart:

Blessed are the pure in heart,

For they shall see our God.

The secret of the Lord is theirs,

Their soul is Christ's abode.

Still to the lowly soul

He doth himself impart,

And for his dwelling and his throne

Chooseth the pure in heart.

Unfortunately we were plagued once again with sound system gremlins today. I'm honestly sick of it, the speakers and microphones are always barely working or not working. Apparently fixing it properly would cost tens of thousands of dollars the parish doesn't have. I don't know what can be done, but it's very frustrating.

Part of my job as an educator is to create situations where my students will be stressed, they will struggle, they might get frustrated, they might even hate me (although that's rare). My mentor Kai Engelhardt said that part of his job was to "torture students". It's a joke of course but there is a kernel of truth there: particularly for learning skills like debugging, there's no better way to learn than by trying to reason your way out of a buggy mess of your own creation. Inflicting this kind of stuff on students is actually kind of essential to education.

A lot of students these days are totally unused to feeling stuck. I asked my Structured Programming students who failed my midterm test the other week how they studied. Many of them actually did quite a lot of practice! But the moment they encountered a bug they couldn't immediately fix, they turned to the bots to solve their problem for them. They read and understood what the bot did, and they conflated that with being able to do it themselves.

Part of the reason these bots are hurting education because they undercut my ability to inflict (educational, non-excessive) stress on my students. I used to design effective programming courses that would keep the stress levels low enough to avoid demoralising students but high enough that they had to engage and work and learn. Now if stress levels go over a certain (low) threshold, all the work gets done by AI unless it's in an invigilated exam, which I used to avoid because they're stress spikes. I don't have a good solution. Just very unhappy.

I found this excellent mastodon thread where someone was brave enough to have a look at the leaked Claude Code source code. Anthropic proudly boasted that much of Claude Code was written by Claude Code — and it definitely shows, and not in a good way. One of the most atrocious code bases I've ever seen. I guess they anticipate going out of business before they have to maintain this crap.

Dómine ne longe fácias auxílium tuum a me, ad defensiónem meam áspice: líbera me de ore leónis, et a córnibus unicornuórum humilitátem meam.

For the first three ferias of Holy Week, I sang gregorian chants (mostly various lenten introits) for the introit and recessional of our contemplative evening masses at All Saints Ainslie. On the Wednesday, I was joined by Lynda Tooth on piano and we performed Dowland's In this trembling shadow:

In this trembling shadow, cast

From those boughes which thy winds shake

Farre from humane troubles plac’d

Songs to the Lord would I make

Darknesse from my minde then take

For thy rites none may begin

Till they feele thy light within.

Nos autem gloriári opórtet, in cruce Dómini nostri Iesu Christi: in quo est salus, vita et ressuréctio nostra: per quem salváti, et liberáti sumus.

Adorámus te, Christe, et benedícimus tibi, quia per crucem sanctam tuam redemísti mundum.

The triduum at All Saints Ainslie consisted just of two main services: the Mass of the Lord's Supper on the Thursday night, followed by the Liturgy of the Passion the following morning. On Thursday we sang I Give You a New Commandment by Nardone during the foot washing:

I give to you a new commandment;

A new commandment I give to you:

That you love one another,

Love one another as I have loved you.

(Ubi cáritas et vera, Deus ibi est)

(Congregávit nos in unum Christi amor)

(Exultémus et in ipso iucundémur)

(Timeámus et amémus Deum vivum.)

(Et ex corde diligámus nos sincéro.)

Amen.

As well as Duruflé's Ubi Caritas during communion, with a very similar but slightly different text:

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.

We weren't high church enough to do a proper Eucharistic procession, but there was a stripping of the altar afterwards with the recitation of Psalm 22. St. Michael and All Saints showed us how it's done with procession, veneration, stripping of the altar, the cleaning of the altar with water and wine, then Fr. Oliver Brewer-Lennon dramatically threw aside the brush used to clean the altar, smashed the old Paschal candle on the sanctuary steps, locked shut the sanctuary gates, tied them with his stole, and ran away (cf. Matthew 26:56), plunging the church into darkness.

The following Good Friday liturgy consisted primarily of the veneration of the Cross and the distribution of the Eucharist which was consecrated the night before. For veneration, we sang first the Victoria Reproaches:

O my people, what have I done to you?

Or in what way have I offended you?

Answer me.

Ἅγιος ὁ Θεός, Holy God,

Ἅγιος ἰσχυρός, Holy and Strong,

Ἅγιος ἀθάνατος, ἐλέησον ἡμᾶς.

Holy and Immortal One, have mercy upon us.

Then we sang Leighton's Solus ad Victimam:

Alone to sacrifice thou goest, Lord,

Giving thyself to death, whom thou hast slain.

For us thy wretched folk is any word?

Who knew that for our sins this is thy pain?

For they are ours, O Lord, our deeds,

Why must thou suffer torture for our sins?

Let our hearts suffer in thy Passion, Lord,

That very suffering may thy mercy win.

This is the night of tears, the three days' space.

Sorrow abiding in the eventide,

Until the daybreak with the risen Christ,

And hearts that sorrowed shall be satisfied.

So may our hearts share in thine anguish, Lord,

That they may sharers of thy glory be;

Heavy with weeping may the three days pass,

To win the laughter of thine Easter Day.

During the distribution of communion we sang O vos omnes from Victoria's Tenebræ responsories.

O vos omnes qui tránsitis per viam,	O all you people that travel by this road,
Atténdite et vidéte!	Look and see
Si est dolor símilis, sicut dolor meus.	Whether there is any sorrow like my sorrow.
Atténdite, univérsi pópuli et vidéte dolórem meum	Look, all you people, and see my anguish.
Si est dolor símilis, sicut dolor meus.	Whether there is any sorrow like my sorrow.

RESURREXI, et adhuc tecum sum, allelúia: posuísti super me manum tuam, allelúia: mirábilis facta est sciéntia tua, allelúia, allelúia.

For Easter this year the church at All Saints Ainslie was filled with flowers, which was lovely. We had a vigil service at night followed by a service in the morning. Sadly the Vigil service didn't include a litany, but we sang Holy is the True Light at the vigil:

Holy is the True Light, and passing wonderful,

Lending radiance to them that endured

In the heat of the conflict.

From Christ they inherit a home of unfading splendour,

Wherein they rejoice with gladness evermore. Alleluia!

We also sang the Easter inaugural Gloria from the Darke Mass in F, both in the vigil and the Sunday Mass.

For the Sunday Mass we sang Ouseley's From the Rising of the Sun:

From the rising of the sun

To the going down of the same,

My Name shall be great among the Gentiles,

And in ev'ry place incense shall be offer'd up unto my Name:

For My Name shall be great among the heathen,

Thus saith the Lord!

I was also given the honour and privilege to once again proclaim the resurrection during the vigil, video below. This chant is my own version by expurgating some bits from the Roman Missal for length. I got a lot of compliments afterwards; although I can detect a few wobbly notes, I think my delivery is improved compared to last year.

This is a special edition of Church Music Corner where I share the programme for our Lenten Concert, In the Midst of Life, that happened today at All Saints Ainslie.

The concert opened with some lovely piano playing by Lynda Tooth followed by Gibbons' Drop, Drop Slow Tears. Then we sang some music from the English renaissance: Farrant's Call to Remembrance, Morley's Nolo Mortem Peccatoris, the Agnus Dei from Byrd's Mass for Four Voices, and Tallis' Hear the Voice and Prayer. Then, to give us a break, Lynda played variations on the theme of Amazing Grace on the piano, followed by the more dramatic fare of the concert: Anerio's Christus factus est, Victoria's O vos omnes, Purcell's Funeral Sentences for Queen Mary (from which the title of the concert is drawn), Attwood's Turn thy Face with Dan Walker singing the solo section, Goss' O Saviour of the World, Stainer's God So Loved the World and finally Lloyd's View me, Lord. For an encore we sang the Nunc Dimittis from Gibbons' Short Service.

The concert was quite well attended and raised some much needed funds for the music of the church. We got a lot of positive feedback, I think the concert went very well. Thanks especially to our guest singers, Dan Walker and Patrick Baker!

Hosánna fílio David, benedíctus qui venit in nómine Dómini. Rex Israël: Hosánna in excélsis.

Púeri Hebræórum, portántes ramos olivárum, obviavérunt Dómino, clamántes et dicéntes: Hosánna in excélsis.

Púeri Hebræórum vestiménta prosternébant in via, et clámabant dicéntes: Hosánna fílio David, benedíctus qui venit in nómine Dómini.

This Palm Sunday at All Saints Ainslie went rather well considering that we were all exhausted from our concert the night before. We sang Mathias' Lift up your heads:

Lift up your heads, O ye gates:

And be ye lift up, ye everlasting doors:

And the King of Glory shall come in.

Who is this King of Glory?

The Lord, strong and mighty,

The Lord, mighty in battle.

Lift up your heads, O ye gates:

Even lift them up, ye everlasting doors:

And the King of Glory shall come in.

Who is this King of Glory?

The Lord of Hosts, he is the King of Glory.

On the 28th of March (the same day as our choir concert), we have the ANU open day. I'll be there in the morning, showcasing some of my retro computer collection. I decided to write a 140KB program for my Apple IIe (just enough to fit on one floppy image) that prospective students can use to learn about our degree programmes.

This was about 1000 lines of assembly: the entire thing is actually graphics, I don't use the Apple II text mode at all. It's actually quite impressive that the Apple IIe is fast enough to do this kind of bitmap rendering. But it truly is a bizarre system: the addressing for the bitmap data is super weird (all over the place), and each byte of bitmap data is 7 (not 8) pixels of data. Still, it means you can do some impressive graphics considering when the first Apple II came out.

It also has a screensaver to stop the burn in on my amber monochrome monitor (which has the right colours for ANU).

I really recommend this article by Paulette D. Koronkevich. It perfectly expresses some of the same thoughts that I've been having about CS, both research and teaching, in this AI-polluted age.

I am only in this business because of the people. My PhD advisor Gabi and her husband Manuel, my mentor Kai, my collaborators Rob and Peter and Christine and Zilin, my colleagues Ohad and James and Sam, and most of all my students over the years, among whom in particular I would name Andrew, Jiyeong, Tammy, Emmett, Amy, Ke and Rayhana.

Iudica me Deus, et discérne causam meam de gente non sancta: ab hómine iníquo et dolóso éripe me: quia tu es Deus meus, et fortitúdo mea.

This final Sunday before Holy Week at All Saints Ainslie was an Evensong sunday, so I sang for the morning service and directed our choir for evensong. In the morning I sang Dowland's In this trembling shadow accompanied by Callum Tolhurst-Close on the organ.

In this trembling shadow, cast

From those boughes which thy winds shake

Farre from humane troubles plac’d

Songs to the Lord would I make

Darknesse from my minde then take

For thy rites none may begin

Till they feele thy light within.

For Evensong, I sang the Venite chant followed by the Choir singing Stainer's Hail, Gladdening Light, ferial preces and responses, my own tonus peregrinus arrangement with organum for the Magnificat and the Nunc Dimittis from Orlando Gibbons' Short Service. For the anthem we sang Wesley's Lead Me, Lord. This was the first time I've directed a choir for Evensong.

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.

Perhaps I should consolodate all of my previous posts linking to articles discussing various aspects of why LLMs are so unconscionable to me:

1. Open Letter against LLMs in Education
2. Old Man Yells at Cloud
3. "AI is Destroying Learning Itself"
4. It's rude to show AI output to people.

This post is adding to their number. William J. Bowman recently wrote up this excellent article which really delves into whether LLMs could actually be considered useful. A great point he made is that as the models get "better", they actually require more work to be useful, as finding the problems in their output becomes harder and harder.

I was also relieved to see that AI is even less popular than ICE in the US (although I was slightly annoyed by the headline of the article, which claims that people hate AI more than ICE, a claim not supported by the poll, which does not measure intensity of dislike).

Also Anthony Moser wrote this excellent piece that was very cathartic for me to read.

Finally, I was glad to see this list of software that has pledged not to accept AI contributions and not to integrate generative AI features. While most of the software on this list is not useful to me at present, I hope it takes off and grows. I do have a very brutal approach: if any software I use tries to integrate AI features, I immediately cut it out of my workflow, no matter how essential. And, if a project accepts AI-authored contributions, I'm on high alert for any possible replacement. This is, for example, why I stopped using ghostty.

Lætáre Ierúsalem: et convéntum fácite omnes qui dilígitis eam: gaudéte cum lætítia, qui in tristítia fuístis: ut exultétis, et satiémini ab ubéribus consolatiónis vestræ.

This was a fairly routine Sunday at All Saints Ainslie, where we sang Gibbons' Drop, Drop Slow Tears:

Drop, drop slow tears

And bathe those beauteous feet,

Which brought from heav'n the news and Prince of Peace.

Cease not, wet eyes,

His mercies to entreat,

To cry for vengeance, sin doth never cease.

In your deep floods

Drown all my faults and fears,

Nor let His eye see sin, but through my tears.

Next week is Evensong (I'll cantor for the morning mass) and the following week is our concert, In The Midst of Life. Please do come along!

Growing increasingly frustrated with the Apple mail client's seemingly unfixable inability to search for emails I just read, I made the switch to MailMate, a good old-fashioned Mac OS X-style app with a lot of useful features, good performance, and, most importantly, working search. Of course, ANU in their infinite wisdom have not seen fit to bless MailMate as an allowed client on their OAuth server, but this is nothing that a little davmail can't fix...

In general, the quality of software on the Mac is getting worse, primarily because a large amount of it isn't even for the Mac (and secondarily because Apple themselves are enshittifying their software and their design guidelines). I'm tired of running 18 instances of Chromium to do basic tasks. This is why I continue to use Nova, TextMate, MailMate, etc. I would use Orion too, except for its jankiness and poor performance compared to Zen. The other major motivation is my aversion to the dreaded bots and those who use them, which is why I moved away from ghostty and to alacritty lately, although I'd welcome suggestions there.

As part of my embrace of well-designed old Mac software, I've started using TextMate again. I made a bundle for building Forester forests that supports completion using forester complete (not LSP, as TextMate predates that).

The bundle can be downloaded from my git repository on tangled.

Last week I auditioned for Coro, a festival concert choir located here in Canberra. I'm delighted to announce that they have invited me to sing with them starting with Motets, their first concert for 2026, scheduled in May.

Oculi mei semper ad Dóminum, quia ipse evéllet de láqueo pedes meos: réspice in me, et miserére mei, quóniam únicus et pauper sum ego.

This Sunday our director was hit with the double-whammy of being both sick and busy, so the choir at All Saints Ainslie was under my (figurative) baton as we sang Saint-Saëns' Ave Verum Corpus, a piece new to me:

Ave verum corpus natum de María Vírgine;	Hail, true body, born of the Virgin Mary;
Vere passum, immolátum in cruce pro hómine;	True suffering, sacrificed on the cross for Man;
Cuius latus perforátum unda fluxit sánguine	From whose pierced side flowed waves of blood,
Esto nobis prægustátum in mortis examine.	Be for us a foretaste in death's trial.

Our organ scholar Lillian also very successfully played for the entire service for the first time. Congratulations to her!

I have taken on another PhD student, Kai Phan, who (at least to start) will conduct some investigations into incorrectness logic, along with me, Xin Lu, and Peter Höfner. Welcome, Kai!

Edwin Park, a new honours student, has also arrived from University of Melbourne to do an honours project with me here at the ANU. We are looking at program calculational techniques such as Carroll Morgan's refinement calculus, and exploring proof-assistant-integrated program calculation techniques.

I began teaching my lectures for Structured Programming over the last week. To my surprise, despite being the same cohort for which I saw soul-destroyingly low attendance last semester, attendance this time was surprisingly decent. Perhaps it's the higher perceived difficulty of the course, the nicer weather, or the slightly more convenient location. Whatever the cause, I'm glad to actually have sufficient students to engage in a conversational lecture.

I have a bit of a sowing-and-then-reaping issue though. I designed the course outline to include weekly lab exercises, three homework tasks, and two mid-term exams. This is all well and good, except now I have to make all of this material. I'm very overwhelmed but well supported by some good tutors including Xin Lu, Kai Phan, Carlo Zancanaro and others.

Tibi dixit cor meum, qeæsívi vultum tuum, vultum tuum Dómine requíram: ne avértas fáciem tuam a me.

Reminíscere miseratiónum tuárum, Dómine, et misericórdiæ tuæ, quæ a saéculo sunt: ne unquam dominéntur nobis inimíci nostri: líbera nos Deus Israel ex ómnibus angústiis nostris.

This Sunday our director was away at All Saints Ainslie so I directed us for the Agnus Dei from Byrd's Mass for Four Voices, one of my favourite pieces:

Agnus Dei, qui tollis peccáta mundi, miserére nobis.	Lamb of God, that taketh away the sins of the world, have mercy upon us.
Agnus Dei, qui tollis peccáta mundi, miserére nobis.	Lamb of God, that taketh away the sins of the world, have mercy upon us.
Agnus Dei, qui tollis peccáta mundi, dona nobis pacem.	Lamb of God, that taketh away the sins of the world, grant us peace.

I also auditioned for the Coro choir. I think I stuffed up the sight reading, but I'll hope for the best.

I had to head to the office today even though it's a Saturday to prepare for my upcoming Structured Programming course, but I was surprised to see Lunar New Years festivities had been transferred to the weekend.

I saw the Dragon and Lion dances as well as some other performances from Chinese and Vietnamese residents of Dickson, and the Canberra Yut Hung Kung Fu school:

In the nearby market stall there was a Korean 호떡 vendor. From our conversation I gathered that there were Korean 설날 events there as well, but in the morning and I was already too late. Oh well, the 호떡 was delicious though!

Miseréris ómnium Dómine, et nihil odísti eórum quæ fecísti, dissímulans peccáta hóminum propter pæniténtiam, et parcens illis, quia tu es Dóminus Deus noster.

This Ash Wednesday was my second at All Saints Ainslie, and I intoned the Trisagion again this year. We had a decent compliment of choristers to perform Duruflé's Ubi Caritas:

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 gathers us as one,
Exultémus et in ipso iucundémur	Let us rejoice and be glad 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.

As well as Gibbons' Drop, Drop Slow Tears which is just a lovely poem:

Drop, drop slow tears

And bathe those beauteous feet,

Which brought from heav'n the news and Prince of Peace.

Cease not, wet eyes,

His mercies to entreat,

To cry for vengeance, sin doth never cease.

In your deep floods

Drown all my faults and fears,

Nor let His eye see sin, but through my tears.

For this Lent I am making some private observances and sacrifices, but I will also be singing the evening office (either Roman or Scottish Episcopal) every day of this Lent. This Sunday will be a choral Evensong!

Invocábit me, et ego dixi exáudiam eum: erípiam eum, et glorificábo eum: longitúdine diérum adimplébo eum.

This Sunday was a busy one for me, as the choir of All Saints Ainslie sings Evensong now on the final Sunday of the month. I, along with a few of our other male singers, sang for the morning mass without the rest of the choir. I sang a special tonus peregrinus gospel acclamation, and for an anthem I sang Tallis' Why Fumeth in Sight, the famous Theme of Ralph Vaughan Williams' Fantasia fame. I've linked to a recording of me singing the first verse.

Why fumeth in sight: the Gentils spite,

In fury raging stout?

Why taketh in hond: the people fond,

Vayne thinges to bring about?

The kinges arise: the lordes devise,

in counsayles mett therto:

Agaynst the Lord: with false accord,

against his Christ they go.

Let us they say: breake downe their ray,

of all their bondes and cordes:

We will renounce: that they pronounce,

their loores as stately lordes.

But God of might: in heaven so bright,

Shall laugh them all to scorne:

The Lord on hie: shall them defie,

they shall be once forlorne.

Then shall his ire: speake all in fire,

to them agayne therfore:

He shall with threate: their malice beate,

in his displeasure sore.

Yet am I set: a king so great,

on Sion hill full fast:

Though me they kill: yet will that hill,

my lawe and worde outlast.

For Evensong we sang Psalm 51 to a nice Anglican chant, and the Nunc Dimittis from Gibbons' Short Service. We didn't get the Magnificat ready in time, so Alasdair and I just sang an antiphonal plainchant Magnificat to the tonus peregrinus. For the anthem, we sang an old favourite of mine, Morley's Nolo Mortem Peccatoris:

In my work with Rayhana Amjad and Rob van Glabbeek, I've been thinking a bit about the space of linear-time temporal properties \Sigma ^\omega . There are a lot of results about this, some of which we're still working on proving. While the canonical account will be in our forthcoming journal paper and Rayhana's PhD thesis, I'm going to start writing a research notebook on this topic. I've decided to do this rather than blog about our results, because it's more in the spirit of Zettelkästen (Zettelkastengeist?) — the post I had in mind ended up ballooning in size because it needed so much context. Instead, I will just fill in the notebook including our current conjectures.

Currently, there isn't much there, just some basic definitions from Defining Liveness. But I will eventually hopefully have a fairly well-developed summary of a lot of the work in this area over there.

Tibi dixit cor meum, quæsívi vultum tuum, vultum tuum Dómine requíram: ne avértas fáciam tuam a me.

Esto mihi in Deum protectórem, et in locum refúgii, ut salvum me fácias: quóniam firmaméntum meum, et refúgium meum es tu: et propter nomen tuum dux mihi eris, et enútries me.

This Sunday was bizarrely called the Sunday of the "Transfiguration", despite that not being the actual feast of the Transfiguration. It's because my church All Saints Ainslie is hewing to the Revised Common Lectionary. I entitled this post Quinquagesima Sunday because that's what is listed in the Scottish Book of Common Prayer (and I am a Scottish Episcopalian). I joined the Ainslie choir for the first time in 2026. We performed Ouseley's From the Rising of the Sun:

From the rising of the sun

To the going down of the same,

My Name shall be great among the Gentiles,

And in ev'ry place incense shall be offer'd up unto my Name:

For My Name shall be great among the heathen,

Thus saith the Lord!

I also received some CD recordings from John Kitchen at Old St. Paul's while I was in Edinburgh, that I took the time to listen to recently. Calum Robertson, who plays the organ at Old St. Paul's, wrote a beautiful anthem from this moving poem by Irene Zimmerman:

The poem, at least to my reading, seems to clearly advocate for women's ordination, despite the author's communion opposing the same.

I came across this article by Alex Martsinovich which I thought captured very well one of the main objections I have to LLMs as a technology. It used to be that every piece of text, even down to a road sign, was written by a human somewhere with the intention of communicating something to you, the reader — what Alex calls "proof of thought". Thanks to LLMs, this fundamental property of language has been irrevocably destroyed: a massive tragedy in my view.

Suscépimus Deus, misericórdiam tuam in médio templi tui : secúndum nomen tuum Deus, ita et laus tua in fines terræ: iustítia plena est déxtera tua.

For this special feast at St. Michael and All Saints (which, per Fr. Oliver's policy, was not transferred to the Sunday), I offered to sing the traditional Gregorian chant propers for the mass, which I had typeset conveniently in Forester for easy reading. Despite the fact that I had a cold, I got a lot of compliments about my chanting and I feel it made the service really special. I also enjoyed a non-alcoholic pint with Fr. Oliver afterwards.

Veníte adorémus Deum, et procidámus ante Dóminum: plorémus ante eum, qui fecit nos: quia ipse est Dóminus Deus noster.

This Sunday I once again sang at both St. Michael and All Saints and Old St. Paul's, despite a cold preventing me from intoning the propers or singing at full voice. In the morning we sang Wood's Hey You, the Middle Ball:

O thou the central orb of righteous love,

Pure beam of the Most High,

Eternal Light of this our wintry world,

Thy radiance bright awakes new joy in faith,

Hope soars above.

Come, quickly come and let thy glory shine,

Gilding our darksome heav'n with rays divine.

Thy saints with holy lustre round thee move,

As stars about thy throne, set in the height

Of God's ordaining counsel,

As thy sight gives measured grace to each.

Thy power to prove.

Let thy bright beams disperse the gloom of sin,

Our nature all shall feel eternal day,

In fellowship with thee,

Transforming day to souls erewhile unclean,

now pure within.

Amen.

We also sang Victoria's Missa O Quam Gloriosum for a mass setting. In the evening, in a rare exception to the normal Evensong service, Old St. Pauls instead had an event to introduce the choir and congregation to the new Revised English Hymnal.

I have previously written extensively about my struggles with faith and the particular mode of agnostic faith that I hold. Recently, Fr. Oliver Brewer-Lennon was kind enough to host me at his home for hours where we had a wide-ranging conversation, including about my faith. For the first time in my life I found a priest who I feel I can rely upon for spiritual direction and who also is just a good friend. He offered a compelling solution to my census dilemma — I can just write "Scottish Episcopalian" on the form. Surely if people can write Jedi as their religion, Scottish Episcopalianism would be acceptable. Next time I visit Edinburgh I will probably take part in a ceremony where I can be officially received into the church. Even though I am thousands of kilometres away usually, I can still call St. Michael and All Saints my parish and Oliver Brewer-Lennon my priest.

He was also nice enough to give me free access to the church whenever I want to use it, so I have been chanting the evening office there according to the Use of Sarum. To avoid keeping 17 places open in 3 books simultaneously, I transcribed large parts of the Sarum vespers and compline office into Forester. You can see the results here for example, but there are more that can be found by searching "Ordo". They use my chant plugins. Fr. Oliver will join me for the vespers and compline of St. Blaise next week.

On the way back from our chat I stopped by a charity shop and got this old illustrated KJV bible for free:

Laetétur cor quæréntium Dóminum : quaérite Dóminum, et confirmámini: quaérite fáciem eius semper.

This Sunday I once again sang at both St. Michael and All Saints and Old St. Paul's. Old St. Pauls transferred Candlemas (the Presentation of the Lord) to Sunday, so the evensong was a special one, but the morning mass was an ordinary time mass. In the morning we sang Bach's O Jesu Christ, meins Lebens Licht:

O Jesu Christ, meins Lebens Licht,	Lord Jesu Christ, my life and light,
Mein Hort, mein Trost, mein Zuversicht,	My strength, my stay, my day-star bright,
Auf Erden bin ich nur ein Gast, :	On earth I have no home or rest,
Und drückt mich sehr der Sünden Last.	By all my grievous sin oppressed.

I cantored for the propers. For the Mass setting, we sang the St. Anne Mass by Sir James MacMillan.

In the evening, we began with a Stainer anthem I'm sure I've done before but I'm not sure when, then this Mozart Magnificat (for which I sang the tenor part in the brief solo quartet sections), a 'Mozart' (actually John Kitchen) Nunc Dimittis, for which no recording exists but can be heard on our livestream. Finally for an anthem we sang the very challenging but interesting Rutter Hymn to the Creator of Light:

Glory be to thee, O Lord, glory be to thee,

Creator of the visible light,

the sun’s ray, the flame of fire;

Creator also of the light invisible and

intellectual:

that which is known of God, the light invisible.

Glory be to thee, O Lord, glory be to thee,

Creator of the light.

for writings of the law, glory be to thee:

for oracles of prophets, glory be to thee:

for melody of psalms, glory be to thee:

for wisdom of proverbs, glory be to thee:

experience of histories, glory be to thee:

a light which never sets.

God is the Lord, who hath shewed us light.

Light, who dost my soul enlighten;

Sun, who all my life dost brighten;

Joy, the sweetest man e’er knoweth;

Fount, whence all my being floweth.

From thy banquet let me measure,

Lord, how vast and deep its treasure;

Through the gifts thou here dost give us,

As thy guest in heaven receive us.

As usual we did John Kitchen's Divine Praises at the end during the Benediction, which was a magical experience when I first heard it in the congregation of OSP years ago.

Today in Sydney I saw David Byrne's concert tour, Who is the Sky?. The guy has incredible energy, even now that he's in his seventies. While he's not as active as he was in Stop Making Sense, he is still a mesmerising performer. The setlist included a surprisingly large amount of Talking Heads classics: Houses in Motion (which was simply amazing), Life During Wartime, And She Was, Slippery People, This Must Be The Place, Once in a Lifetime, Burning Down the House, Heaven, Psycho Killer and Nothing but Flowers. There were also a few solo tracks I recognised: Like Humans Do, Strange Overtones and Everybody's Coming to My House.

What stands out to me is the extremely tight choreography and use of the stage space. The entire performance was just the performers carrying all their instruments like a marching band while wearing blue jumpsuits, with various images projected on the screens behind them. Somehow, it never got old. It was an utterly captivating performance, and the music was fantastic of course.

Dóminus secus mare Galiláeae vidit duos fratres, Petrum et Andréam, et vocávit eos: Veníte post me: fáciam vos fíeri piscatóres hóminum.

Adoráte Deum omnes Angeli eius audívit, et lætáta est Sion: et exsultavérunt fíliæ Iudæ.

This Sunday I sang with two choirs: St. Michael and All Saints for the morning mass and Old St. Paul's for evensong, which included lucernarium and benediction of the Blessed Sacrament. In the morning we sang Franck's Panis Angelicus and a simple choral mass setting whose composer I can't now recall.

Panis angelicus	Bread of angels
fit panis hominum;	Becomes the bread of men;
Dat panis cœlicus figuris terminum:	The heavenly bread ends the old figures:
O res mirabilis!	O wondrous thing!
Manducat Dominum	To eat of the Lord
pauper, servus et humilis.	The poor, the servant, the humble.

I cantored for the propers. In the evening, as it's the Conversion of St. Paul, the namesake of the church, we performed some ambitious repertoire, including the Bairstow Magnificat and Nunc Dimittis, as well as Palestrina's Magnus Sanctus Paulus for eight voices, which I can't find a recording of anywhere.

Magnus sanctus Paulus,	Saint Paul the Great,
vas electiónis	The vessel that was chosen,
vere digne est glorificándus,	truly worthy to be praised,
qui et thronum duodécimum méruit possidére.	who merited the twelfth throne.
intercéde pro nobis ad Deum,	Intercede for us to God,
qui te elegit, ut digni efficiamur gratia Dei.	who chose thee, that we may be made worthy of the grace of God.

We also performed Widor's Tantum Ergo for the Benediction.

In between those two services I also stopped in to hear Evensong at St. Mary's Episcopal Cathedral in Edinburgh's west end. The choir there is very good, and I always like attending evensong there, although one of the sopranos was annoyingly out of tune this time.

I was baptised into the Roman church and confirmed in the faith by a high-ranking prelate in the Church at St. Mary's Cathedral, where I sang in the choir for over a decade. I have attended and sung at traditional Latin masses, I'm very familiar with catholic theology and liturgy, and I even won an award for Catholic studies at my cathedral high school. I love the Latin language, I love the traditions of the Church, particularly its musical tradition, and I love the universality of the Roman church. Still, I left the Church gradually as I became preoccupied with other aspects of my life, and then various pedophilia scandals, including of the headmaster of my school and of the prelate who confirmed me, were the nails in the coffin. I stopped regularly attending any church.

Gradually, particularly after moving to Edinburgh, as I accrued a greater understanding of my own peculiar mode of belief, I returned to regular churchgoing, but this time at an extremely "Anglo-catholic" Scottish Episcopal church, although I'd still pop into the Edinburgh Jesuit church for a Catholic mass now and again. The main thing that prevented me from wholly returning to Rome (aside from my personal affinity to that SEC church), was that I just couldn't bring myself to assent to the doctrines of the Roman church. While I'm not a fan in general of the Articles of Religion for the Church of England, article XIX has a point:

As the Church of Jerusalem, Alexandria, and Antioch, have erred; so also the Church of Rome hath erred, not only in their living and manner of Ceremonies, but also in matters of Faith.

I don't think this point is particularly controversial, even among many lay Roman Catholics. It is hard to say with a straight face that the Church has always taught the right doctrines and that all of its authoritative teachings are irreversible, and yet the First Vatican Council effectively commits the Roman Church to precisely that position. Even where infallibility is narrowly defined, the broader assumption remains: that the Church cannot, in any meaningful sense, have been wrong in its teaching. This position is so ludicrous that it seems that recent popes quietly admit that it's not true while upholding continuity of magisterial teaching in public: what looks, in hindsight, like error must always be re-described as development, ambiguity, or misapplication. This makes genuine doctrinal correction (as opposed to "reinterpretation") impossible.

So, what would the Roman church have to do to win me back over?

• Overturn Vatican I, admit error, and confess wrongdoing. There is no way that any of the other changes in this list could be made without first admitting that the Church was wrong.
• Equality between genders, including for holy orders and the episcopate. Recalling Galatians 3:28 "In Christ there is no male or female", the argument that women cannot act in persona Christi for the purposes of the sacraments seems ridiculous. As for the episcopate, claiming that the gender of the apostles was theologically important rather than merely socially convenient seems completely scripturally and logically unfounded. Of course the apostles were male: the society of the time would have broadly rejected female philosophers, teachers, or evangelists. Their maleness gave them some temporal authority, but that doesn't mean that their maleness was in any way necessary for their sacramental authority. And, there's significant evidence that before the Constantinian adoption of Christianity into the Imperial system, early Christians had many female religious leaders, anyway — not least of which is Mary Magdalene, sometimes called Apostle to the Apostles.
• Welcome and equality for LGBTQ+ individuals and couples, and apologise for harm done. There are ministries and pockets of the Church were gay people are welcome, because Christ is always on the side of those who are marginalised and oppressed. But, in general, the Church remains a deeply homophobic and transphobic institution (despite the presence, throughout the Church’s history, of much-lauded figures whose sex lives would sit very uneasily in the Church’s proscriptive framework). The Church would have to revise its exclusionary attitudes before I would consider fully returning. This would include extending the sacrament of matrimony to gay couples.
• Eliminate overscrupulous sin accounting, particularly regarding sexual ethics. The Church produces elaborate frameworks for evaluating sin, and overformalises what it understands sin to be. In particular, the elaborate framework of sexual ethics based on "natural law" gets really weird fast. I'm not saying that there's no such thing as sinful sexual behaviour, but declaring contraception sinful (as an example) seems both scientifically illiterate and needlessly overproscriptive. The Church shouldn't be in the business of classifying more and more and more human activities into various levels of sinfulness. The fullness of the law is love, not a bureaucratic accounting of how many rules you break.
• Distinguish between what is sinful and what ought to be illegal. The Church has already done this to a certain extent, pushing for the decriminalisation of homosexuality in those places where it is still illegal, but I think this should be applied more generally. For example, while I'm not taking a firm position here, I'd be willing to accept that abortion might be a sin, even a grave sin, at least in most cases. I don't think it should be illegal, however, because the harm that is done seems by most measures far greater when abortion is illegal than when it is legal. Medical grey areas shouldn't invite legal intervention. The same goes for adultery, blasphemy and many other things that can be declared sinful with a lot of scriptural support but nonetheless shouldn't be banned by the state.
• Recognise the validity of (most) Anglican orders. The Apostolicæ curæ letter of Leo XIII deemed Anglican ordinations invalid because the form and intention of some of the historical ordination rites didn't seem to refer to the sacrificial priesthood that the Roman church maintains. This is clearly a post-hoc rationalisation of the conclusion that he wanted to reach — Anglican orders being invalid — because many of the churches that the Roman Church deems valid, even the Eastern Rite churches within the Roman church itself, also omit some of the important sacrificial language used by the Roman rite. Apostolic succession can pass just as easily through Edwardine Anglicans as it can pass through Arian heretics during the time of St. Hilary. To reject this succession because the Anglican church erred at some points in its history sounds a lot like Donatism. If the Church does recognise these orders, along with the first two changes in my list, there is very little that stands in the way of reunification of these two faiths.

None of these changes that would make a return to Rome conceivable for me can be addressed in isolation, because all of them would require the Church to admit that it has taught wrongly in the past. I'm not holding my breath.

Ultimately, what keeps me from swimming back across the Tiber is not any particular point of disagreement but a deeper structural problem: A church that cannot admit having been wrong in matters of faith cannot meaningfully repent, and a church that cannot meaningfully repent cannot convincingly claim to be guided by the Spirit of truth. I continue to love much of what the Roman Church has given me, but I cannot assent to a vision of the Church that treats its own history as something that must always be explained away rather than, at times, confessed.

As a postscript, I should add that none of the above should be read as a complaint about the Church’s liturgical inheritance, which remains one of the great treasures of Western Christianity. If anything, my frustration is that this inheritance is often treated carelessly or instrumentally, either as a battlefield for ideology or as something endlessly malleable (see The ICEL Lord's Prayer is Terrible). The fact is that here in Australia, finding a reverent, beautiful liturgy in a Catholic church is vanishingly rare — mostly limited to the big cathedrals, and those liturgies outside of the novus ordo milieu: the personal ordinariates and the FSSP Latin Masses, which have congregations that tend greatly towards far-right reactionary ideology. This is an issue of governance, not doctrine. A Church capable of regulating doctrine in extraordinary detail seems strangely incapable of insisting on reverence, beauty, and care in its public worship. This asymmetry only reinforces the impression of an authority structure that is confident where it should be cautious, and timid where it should be firm.

If I still lived in Scotland, answering the Religion question on a census would be easy (at least, easy modulo my peculiar mode of belief): I would simply write "Scottish Episcopalian". The SEC aligns closely with the kind of worship and belief that matters to me — Catholic-style liturgy and theology, reverent sacramental practice, and a progressive, egalitarian, and consistent moral framework. But were I given the same question in Australia, it would be much harder to write "Anglican". The cognate church to the SEC in Australia is fragmented, factionalised, and often incoherent.

Were I to tell a Sydneysider that I was an Anglican, I might be mistaken for a member of the dreaded Sydney diocese — fiercely low-church and conservative. They deny women ordination; they discriminate against LGBTQ+ people; they celebrate the Eucharist with no liturgical reverence, while wearing a suit and tie; they pursue schism with the wider Anglican communion. The small Anglo-catholic outposts that survive in Sydney, like Christ Church St. Laurence, are stuck in a constant struggle against the broader diocese. Even St. James King St, which is more distinctly Anglican in its liturgy, is very much at odds with the diocese, which sometimes seems more like an American evangelical "non-denominational" group than a real Anglican diocese. Other dioceses in the Anglican Church of Australia, trying to maintain unity with this bunch of schismatic agitators masquerading as a diocese, pursue a minimal or compromise-driven theology and liturgy. This constant balancing act prevents the church from taking decisive action on ethical issues like women's ordination or LGBTQ+ inclusion, and liturgy, a tremendous source of beauty and devotion, is often sidelined or distorted (see The ICEL Lord's Prayer is Terrible). The more the church compromises to hold itself together, the less coherent and spiritually compelling it becomes.

Another difficulty I have with Anglicanism is the Thirty-Nine Articles of Religion. I disagree with several key aspects of the Articles: their emphasis on justification by faith alone, their rejection of purgatory and prayers for the dead, their apparent denial of the physical presence in the Eucharist, and their subordination of tradition to Scripture. In the Anglican Church of Australia, clergy are formally required to assent to the Articles, whereas laity generally are not. In practice, however, even among clergy the Articles are often interpreted loosely or ignored, to maintain unity or suit their own personal theological preferences. While this laxity is fortunate for someone like me who disagrees with many of the Articles, it also highlights the church's structural incoherence and inconsistency in both doctrine and governance. The Oxford Movement offers an interpretation of the Articles which is much more Catholic-leaning and far more agreeable to me, but even so, I do not find myself comfortable with the fundamentally Protestant theology that one would get from a basic reading. The Scottish Episcopal Church, thankfully, does not impose the same subscription anywhere (they abandoned the Articles in 1979, after the Relief Act which enforced their subscription was finally repealed), which is one reason it feels much closer to my ideal.

More broadly, the Anglican Communion as a whole lacks a fixed, consistent set of beliefs. In the United States, bishops like John Shelby Spong moved so far away from the faith that they couldn't meaningfully be called Christian, let alone Anglican. In Australia, the aforementioned Sydney Diocese is a hyperconservative low-church enclave in tension with the rest of the Communion. In no sense could these two be said to share the same faith. Across the wider church, there is no guarantee that any given parish or diocese actually adheres to the same theological or moral framework. This absence of a coherent, shared faith makes it difficult to affirm Anglicanism as a whole, even when individual parishes (like CCSL or St. Peter's Eastern Hill) contain aspects I admire.

There are parts of Anglicanism that I genuinely appreciate — mostly, those elements that echo the Catholic tradition rather than the Protestant or uniquely Anglican. The more a parish resembles a reverent, sacramental, and theologically coherent Catholic church, the more it appeals to me. In other words, what I value in Anglicanism is what it shares with Catholicism, not what makes it uniquely Anglican, with one massive exception: The Book of Common Prayer. Its beautiful language, Cranmer's excellent translations of Latin collects, the lovely rhythm of its condensed office and psalter, and its theological subtlety are consistently beautiful, and it remains a singular strength of the Anglican tradition.

Ultimately, I think my ideal Anglican church would end up looking a lot like my ideal Catholic church: reverent, sacramental, inclusive, fearlessly progressive, and theologically catholic; without hubristic claims to infallibility, yet undivided by factional squabbles. When I lay it out this way, it doesn't seem like such a church could exist any time soon. Until then, I will remain vaguely a non-Roman Catholic who worships predominantly at Anglican churches, although I have no idea what I'll write on the next census.

Omnis terra adóret te, Deus, et psallat tibi: psalmum dicat nómini tuo, Altíssime.

This Sunday I sang at my usual All Saints Ainslie, although the choir is still on break. Instead, our soprano Cindy Chen (who played the organ for the hymns) joined me for singing Prätorius' uncommon piece Christe der du bist Tag und Licht (translation is mine):

Christe der du bist tag und licht,	O Christ, thou art both day and light,
Vor dir ist, Herr, verborgen nicht;	For there is, Lord, naught hid from thee;
Du väterliches Lichtes glanz,	Thy fatherly light upon us shine,
Lehr' uns den Weg der Wahrheit ganz.	Teach us thy way of perfect truth.

Cindy and I sang it well, despite many tricky bits!

The clergy and lay canons at St. Peter's Eastern Hill, in addition to letting me sing in their choir, were also kind enough to let me join them for their private divine office, and I've been joining them every day I've been here in Melbourne. I start the day with Matins and Lauds and end the day with Vespers. It's been surprisingly restorative. For one, it stops me from sleeping in later and later which often happens over time when I travel. I plan to do the same thing when I travel to Edinburgh later in the month.

I also attended some services at the lovely Catholic St. Patrick's Cathedral across the road, although I found their service schedule disappointing compared to Sydney's St. Mary's Cathedral. The building itself is beautiful, however:

Also, for completeness' sake I guess, I visited briefly the Anglican St. Paul's Cathedral near Flinders Street Station, but unlike St. Pat's it was quite overrun with tourists. Still much to appreciate in the building itself, however:

I also went to the State Library of Victoria, where in addition to seeing the impressive La Trobe Reading Room I also got to have a look at a few manuscripts that were interesting to me:

The first manuscript pictured above seems to be a chant for the text Levíta Lauréntius, but it doesn't seem to resemble any of the chants from the Solesmes books. I'm not sure where this melody comes from or where it's ended up (if anywhere) in the modern graduals. The next one, in a frame, seems to be a page from a nocturnal or antiphonary, because what starts halfway down the page is Centum quadraginta, an antiphon for the memorial of the Holy Innocents. The third shot, which isn't of a chant book, seems to be a missal of some kind, with a Eucharistic canon on the left and some propers on the right, including the ad te levávi text that immediately signifies the first Sunday of Advent.

Dilexísti iustítiam, et odísti iniquitátem: proptérea unxit te Deus, Deus tuus. Óleo lætítiæ præ consórtibus tuis.

Benedíctus qui venit in nómine Dómini: benedíximus vobis de domo Dómini: Deus Dóminus, et illúxit nobis, allelúia, allelúia.

This Sunday I sang with the choir of St. Peter's Eastern Hill in Melbourne. We sang the Simple Communion Service in F Major by William Harris, for which I can't find a recording online (although the livestream link for St. Peter's isn't bad, and we sang it well). For a motet we sang Marenzio's Tribus miraculis:

Tribus miráculis ornátum, diem sanctum cólimus:	Distinguished by three miracles, this holy day is celebrated:
Hódie stella Magos duxit ad præsépium:	Today the star led the Magi to the manger;
Hódie vinum ex aqua factum est ad núptias:	Today wine was made from water at the wedding;
Hódie in Jordáne a Joánne Christus baptizári vóluit,	Today in the Jordan by John, Christ chose to be baptized
ut salváret nos, Allelúia.	in order to save us, Alleluia.

It was really nice to sing with a choir that was a little more well-resourced, meet some lovely new people, and learn some music that was new to me. I'll be sure to join this choir again whenever I'm in Melbourne!

Ecce advénit dominátor Dóminus: et regnum in manu eius, et potéstas, et impérium.

I was a one-man choir for the mass at All Saints Ainslie today. I sang a Christmas Gloria in place of the usual one from the Dudman mass setting, and for an anthem I sang Cornelius' The Three Kings, where the choir was replaced with a lovely piano accompaniment:

Three kings from Persian lands afar

To Jordan follow the pointing star.

And this the quest of the travellers three,

Where the newborn King of the Jews may be.

Full royal gifts they bear for the king;

Gold, incense, myrrh are their offering.

The star shines out with a steadfast ray,

The kings to Bethlehem make their way,

And there in worship they bend the knee,

As Mary's child in her lap they see.

Full royal gifts they show to the king;

Gold, incense, myrrh are their offering.

Thou child of Man, lo, to Bethlehem

The kings are travelling; travel with them!

The star of Mercy, the star of Grace,

Shall lead thy heart to its resting place.

Gold, incense, myrrh, thou canst not bring;

Offer thy heart to the infant King.

Offer thy heart.

I think it went rather well! I got many compliments during and after the service.

I've also finally added all my Chester-published polyphonic works and the English Church Music books to my Music Index, so the index should be more or less complete for now.

Dóminus dixit ad me: Fílius meus es tu, Ego hódie génui te.

Puer natus est nobis, et fílius datus est nobis: cuius impérium super húmerum eius: et vocábitur nomen eius, magni consílii Angelus.

This Christmas at All Saints Ainslie we reprised Bach's Jesu, Joy of Man's Desiring at the Midnight Mass, this time with an oboe (our oboist also played the descant lines for the classic Willcocks carols):

Jesu, joy of man's desiring,

Holy wisdom, love most bright;

Drawn by Thee, our souls aspiring

Soar to uncreated light.

Word of God, our flesh that fashioned,

With the fire of life impassioned,

Striving still to truth unknown,

Soaring, dying round Thy throne.

Through the way where hope is guiding,

Hark, what peaceful music rings;

Where the flock, in Thee confiding,

Drink of joy from deathless springs.

Theirs is beauty's fairest pleasure;

Theirs is wisdom's holiest treasure.

Thou dost ever lead Thine own

In the love of joys unknown.

There were many many stars visible in the night sky on the way to and from the service. Reminds me of the English version of the Cantique de Noël ("O Holy Night").

Our director Alasdair cantored solo for the Christmas day mass, so we only had to sing for one service. I also tuned into the livestreamed midnight mass at my old haunt St. Michael and All Saints, and got hit with massive liturgical envy. They did all of the ordinaries and propers in Latin with gregorian chant. Some really great liturgy work in general. I plan to sing with them again for two weeks next month!

Deus in loco sancto suo: Deus, qui inhabitáre facit unánimes in domo: ipse dabit virtútem et fortitúdinem plebi suæ.

Dum médium siléntium tenérent ómnia, et nox in suo cursu médium iter habéret, omnípotens sermo tuus, Dómine, de cælis a regálibus sédibus venit.

I got up early to attend the BCP service at St. John's, but was disappointed to see that the service was following the APBA and not the BCP. I think the BCP is only used after January. Furthermore, even by APBA standards the Eucharistic prayer was rushed and insufficiently reverent. Oh well, it is a lovely little church:

Then I walked to All Saints Ainslie, and volunteered at the last minute to cantor for this choirless Sunday mass. I sang an old favourite of mine a capella: The truth sent from above (famously used by Ralph Vaughan Williams in his Fantasia on Christmas Carols):

This is the truth sent from above,

The truth of God, the God of love,

Therefore don't turn me from your door

But hearken all, both rich and poor.

The first thing which I do relate

Is that God did Man create;

The next thing which to you I'll tell:

Woman was made with Man to dwell.

Then after this 'twas God's own choice

To place them both in Paradise,

There to remain from Evil free,

Except they ate of such a tree.

Thus we were heirs to endless woes

Till God the Lord did interpose,

And so a promise soon did run

That he would redeem us by his Son.

And at this season of the year,

Our blest Redeemer did appear.

Here he did live, and here did preach,

Any many thousands he did teach.

Thus he in Love to us behaved,

To show us how we must be saved,

And if you too want to know the way

Be pleased to hear what He did say.

Roráte cæli désuper, et nubes pluant iustum: aperiátur terra, et gérminet Salvatórem.

This muggy Sunday at All Saints Ainslie we sang Prätorius' Es ist ein Ros' entsprungen under my direction. There was also a memorial minute of silence for the victims of the horrific Bondi shooting in Sydney last Sunday.

Es ist ein Ros entsprungen,	There is a rose up-springing,
aus einer Wurzel zart,	from a tender root,
wie uns die Alten sungen,	as the ancients have sung,
von Jesse kam die Art	it comes from Jesse's branch.
und hat ein Blümlein bracht	Its blossom flowering bright,
mitten im kalten Winter,	amidst the cold winter,
wohl zu der halben Nacht.	when half the night remains.
Das Röslein, das ich meine,	This little rose of which I sing,
davon Jesaja sagt,	of which Isaiah spoke,
hat uns gebracht alleine	was brought to us solely by
Marie, die reine Magd.	Mary, the pure maiden.
Aus Gottes ew'gem Rat	By God's eternal plan,
hat sie ein Kind geboren	a child was born to her
und blieb doch reine Magd.	but she remained a pure Maiden.
Das Blümelein so kleine,	That little blossom, so tiny,
das duftet uns so süß,	that to us smells so sweet,
mit seinem hellen Scheine	with its bright shining
Vertreibt's die Finsternis.	drives away the darkness.
Wahr' Mensch und wahrer Gott,	True man and truer God,
hilft uns aus allem Leide,	He aids us from all suffering,
rettet von Sünd und Tod.	and saves us from sin and death.

Edit: I tuned in to the mass at my old haunt St. Michael and All Saints and discovered that they sang the same anthem (but in English). Nice bit of synchronicity.

Edit 2: I also forgot to mention that last Wednesday, three of us also went to the Goodwin Retirement Village in Ainslie to sing for the Christmas service they held in their chapel, where we sang the Coventry Carol:

Lully, lullay, þow littell tyne childe,

by, by, lully, lullay.

þow littell tyne childe:

by, by, lully, lullay.

O! Sisters too, how may we do

for to preserve this day

this pore yongling for whom we do singe:

by, by, lully, lullay?

Herod, the king, in his raging,

chargid he hath this day,

his men of might in his owne sight,

all yonge children to slay.

That wo is me, pore childe, for Thee

and ever morne and day

for thi parting nether say nor singe:

by, by, lully, lullay.

I use Web Components to make widgets that I can easily emit from Forester documents, such as my Gregorian Chants in Forester and Syntax Highlighting plugins. I noticed that on large pages (such as my weeknotes page) these plugins would sometimes mysteriously fail to load. I later realised that this is because the innerText, innerHTML and textContent properties may not be initialised when the web component is attached to the DOM, if the page is still loading. The solution requires attaching mutation listeners and waiting for the text to be added later. This seems unnecessarily complicated, but anyway, the plugins have been fixed now.

I've already listed a decent number of anti-LLM articles from various perspectives: the technological assault on artistic pursuit, authentic self-development, our social protocols, and on the stability of the economy, but (beyond the open letter itself) I hadn't seen much quality writing on the profound damage this technology is doing to higher education, until I read this current affairs article by Ronald Purser. A lot of it ties in with a general decline in conscientiousness that I think is not only a sign of a sick society, but also a deeply unfulfilling one. It's well worth the read.

Gaudéte in Dómino semper: íterum dico, gaudéte: modéstia vestra nota sit ómnibus homínibus: Dóminus prope est. Nihil sollíciti sitis: sed omni orátione petitiónes vestræ innotéscant apud Deum.

This "Gaudete" Sunday at All Saints Ainslie we had fun singing this medieval carol:

Gaudéte, gaudéte Christus est natus	Rejoice! Rejoice, Christ is born
ex María vírgine, Gaudéte!	of the Virgin Mary, Rejoice!
Tempus adest grátiæ, hoc quod optabámus,	The time of grace has come, of which we wished,
Carmina lætítiæ devóte reddámus!	Let us faithfully render songs of joy!
Deus homo factus est, nátura mirante	God has become Man, nature marvels.
Mundus renovátus est, a Christo regnánte	The world is renewed by the reigning Christ.
Ezechiélis porta clausa per tránsítur	The closed gate of Ezekiel is passed,
Unde lux est orta salus invenítur.	Whence light has risen, salvation is found.
Ergo nostra cóntio psallat iam in lústro,	Now let our assembly sing psalms to him in gladness,
Benedícat Dómino, salus regi nostro.	Let us bless the Lord, greetings to our King.
Gaudéte, gaudéte Christus est natus	Rejoice! Rejoice, Christ is born
ex María vírgine, Gaudéte!	of the Virgin Mary, Rejoice!

The first week of the ANU Logic Summer School has concluded, including my introductory course on Interactive theorem proving. I think the course went well and students learnt a little of what makes theorem proving fun. Chelsea Edmonds will follow on from my course in week 2 with her own course on software verification. I hope I prepared the students well. We went on an excursion to the Tidbinbilla nature reserve (photos of which I have also previously shared on Weeknotes 2025-W27 and Weeknotes 2025-W44).

It was a lot of fun to show some of our visiting students some of the natural landscapes so easily accessible from Canberra. I think we all had a really good day, even though it was sweltering hot.

Populus Sion, ecce Dóminus véniet ad salvándas gentes: et audítam fáciet Dóminus glóriam vocis suæ, in lætítia cordis vestri.

This was a big Sunday at All Saints Ainslie. In the morning a small group of us sang Bach's Jesu, Joy of Man's Desiring:

Jesu, joy of man's desiring,

Holy wisdom, love most bright;

Drawn by Thee, our souls aspiring

Soar to uncreated light.

Word of God, our flesh that fashioned,

With the fire of life impassioned,

Striving still to truth unknown,

Soaring, dying round Thy throne.

Through the way where hope is guiding,

Hark, what peaceful music rings;

Where the flock, in Thee confiding,

Drink of joy from deathless springs.

Theirs is beauty's fairest pleasure;

Theirs is wisdom's holiest treasure.

Thou dost ever lead Thine own

In the love of joys unknown.

But, more significantly, we had our annual Lessons and Carols service. I cantored for the initial Matin Responsory based on a Nunc Dimittis by Palestrina (despite the fact the Carols for Choirs edition says it's based on a Magnificat):

I look from afar,

And lo, I see the power of God coming, and a cloud covering the whole Earth.

Go ye out to meet him and say:

Tell us, art thou he that should come to reign over thy people Israel?

High and low, rich and poor, one with another,

Go ye out to meet him and say:

Hear, O thou Shepherd of Israel, thou that leadest Joseph like a sheep,

Tell us, art thou he that should come?

Stir up thy strength, O Lord, and come

To reign over thy people, Israel.

Glory be to the Father and to the Son, and to the Holy Ghost.

I look from afar,

And lo, I see the power of God coming, and a cloud covering the whole Earth.

Go ye out to meet him and say:

Tell us, art thou he that should come to reign over thy people Israel?

We had several guest singers join us including Rachel Mink and Dan Walker from Luminescence. Rachel sang the initial verse of Once In Royal David's City, after which we processed to the remaining verses. After the first lesson from yours truly, we performed Ord's Adam Lay Ybounden:

Adam lay ybounden, bounden in a bond.

Four thousand winter thought he not too long.

And all was for an apple, an apple that he took,

As clerkes finden written in their book.

Ne had the apple taken been, the apple taken been,

Ne had never our ladye a been heavené queen.

Blessed be the time that apple taken was,

Therefore we moun singen Deo Gracias.

Following another reading, we had one of my favourite Christmas classics, Prätorius' Es ist ein Ros' entsprungen.

Es ist ein Ros entsprungen,	There is a rose up-springing,
aus einer Wurzel zart,	from a tender root,
wie uns die Alten sungen,	as the ancients have sung,
von Jesse kam die Art	it comes from Jesse's branch.
und hat ein Blümlein bracht	Its blossom flowering bright,
mitten im kalten Winter,	amidst the cold winter,
wohl zu der halben Nacht.	when half the night remains.
Das Röslein, das ich meine,	This little rose of which I sing,
davon Jesaja sagt,	of which Isaiah spoke,
hat uns gebracht alleine	was brought to us solely by
Marie, die reine Magd.	Mary, the pure maiden.
Aus Gottes ew'gem Rat	By God's eternal plan,
hat sie ein Kind geboren	a child was born to her
und blieb doch reine Magd.	but she remained a pure Maiden.
Das Blümelein so kleine,	That little blossom, so tiny,
das duftet uns so süß,	that to us smells so sweet,
mit seinem hellen Scheine	with its bright shining
Vertreibt's die Finsternis.	drives away the darkness.
Wahr' Mensch und wahrer Gott,	True man and truer God,
hilft uns aus allem Leide,	He aids us from all suffering,
rettet von Sünd und Tod.	and saves us from sin and death.

After the next reading was the original traditonal arrangement of the Coventry Carol with the crunchy false relation in the cadence.

Lully, lullay, þow littell tyne childe,

by, by, lully, lullay.

þow littell tyne childe:

by, by, lully, lullay.

O! Sisters too, how may we do

for to preserve this day

this pore yongling for whom we do singe:

by, by, lully, lullay?

Herod, the king, in his raging,

chargid he hath this day,

his men of might in his owne sight,

all yonge children to slay.

That wo is me, pore childe, for Thee

and ever morne and day

for thi parting nether say nor singe:

by, by, lully, lullay.

The next reading was followed by O little town of Bethlehem with the Willcocks descant. Then, after the next reading we sang the significantly less common arrangement of the Basque carol Gabriel's Message, also known as the Angel Gabriel or the Most Highly Flavoured Gravy.

The Angel Gabriel from heaven came,

his wings as drifted snow, his eyes as flame;

'All hail', said he, 'thou lowly maiden Mary

Most highly favoured lady, Gloria.'

'For known a blesséd Mother thou shalt be,

all generations laud and honour thee,

thy Son shall be Immanuel by seers foretold;

Most highly favoured lady, Gloria.'

Then gentle Mary meekly bowed her head,

'To me be as it pleaseth God', she said,

'My soul shall laud and magnify his holy name':

most highly favoured lady, Gloria.

Of her, Immanuel, the Christ was born

in Bethlehem all on a Christmas morn,

and Christian folk throughout the world will ever say:

'most highly favoured lady, Gloria.'

After one more reading, we performed what I think was a highlight of the whole service, and one of our best performances, Lauridsen's O Magnum Mysterium:

O mágnum mystérium	O great mystery,
et admirábile sacraméntum,	and wondrous sacrament,
ut animália vidérent Dóminum nátum,	that animals should see the newborn Lord,
jacéntem in præsépio.	lying in a manger.
Beáta virgo, cújus víscera meruérunt	Blessed virgin, whose womb was worthy
portáre Dóminum Chrístum. Alleluia	to bear the Lord Christ. Alleluia

Then we processed out while shepherds washed their socks and ascended to the organ loft for the remainder of the service, where we performed Warlock's Bethlehem Down. I heard that anthem was written on a napkin by an alcoholic and antitheist Peter Warlock in exchange for beer money, and that he died a few years after writing it. But the anthem itself is quite special.

When He is King we will give him the King's gifts,

Myrrh for its sweetness, and gold for a crown,

"Beautiful robes", said the young girl to Joseph

Fair with her first-born on Bethlehem Down.

Bethlehem Down is full of the starlight

Winds for the spices, and stars for the gold,

Mary for sleep, and for lullaby music

Songs of a shepherd by Bethlehem fold.

When He is King they will clothe Him in grave-sheets,

Myrrh for embalming, and wood for a crown,

He that lies now in the white arms of Mary

Sleeping so lightly on Bethlehem Down.

Here He has peace and a short while for dreaming,

Close-huddled oxen to keep Him from cold,

Mary for love, and for lullaby music

Songs of a shepherd by Bethlehem fold.

This was followed by another congregational carol with Willcocks descant, Hark the Herald Angels Sing and our last anthem of the evening, Wood's Hey you! The Middle Ball.

O thou the central orb of righteous love,

Pure beam of the Most High,

Eternal Light of this our wintry world,

Thy radiance bright awakes new joy in faith,

Hope soars above.

Come, quickly come and let thy glory shine,

Gilding our darksome heav'n with rays divine.

Thy saints with holy lustre round thee move,

As stars about thy throne, set in the height

Of God's ordaining counsel,

As thy sight gives measured grace to each.

Thy power to prove.

Let thy bright beams disperse the gloom of sin,

Our nature all shall feel eternal day,

In fellowship with thee,

Transforming day to souls erewhile unclean,

now pure within.

Amen.

Of course, it wouldn't be a Christmas Carols service without the "Word of the Father" chord, so we finished up with Willcocks' arrangement of O Come, All Ye Faithful.

Today I went with many colleagues to Google Sydney for the Sydney Area Programming Languages Interest Group (SAPLING) 2025 meeting. I didn't present anything at the meeting but my PhD student, Xin Lu did a lightning talk introducing her work on incorrectness logic.

It was good to see many colleagues from UNSW Sydney and catch up with some of my former students who were now working for Google.

One of my many bugbears with the Australian Anglican liturgy for the mass (based on A Prayer Book for Australia) is that they adopted the absolutely atrocious "modern" version of the Lord's Prayer from the Vatican's International Commission on English in the Liturgy some time during the 1970s:

Our Father in Heaven,

Hallowed be your name,

Your kingdom come,

Your will be done on Earth as in Heaven,

Give us today our daily bread,

And forgive us our sins,

As we forgive those who sin against us,

Save us from the time of trial,

And deliver us from evil.

(For the Kingdom, the Power and the Glory are yours, now and forever.)

Amen

I won't get into whether or why the doxology should or shouldn't be included in the prayer (although the answer is that it shouldn't), but I think this is an absolutely terrible translation that is so egregiously bad that I mumble the prayer in Latin at that point in the service at All Saints when I sing there.

About 50-60 years ago when the ICEL attempted to make modern translations of liturgical prayers, they had four main goals in mind:

• Accessibility to normal English speakers. Unlike the archaic BCP English which often tends to be poetic, the ICEL liturgy was intended to be straightforward for normal English speakers with no special training to understand.
• Avoiding theological pitfalls. Lines such as "Lead us not into temptation" should be avoided because they imply that God somehow directly tempts us, which is theologically problematic.
• Ecumenism. The liturgy was intended for Roman Catholic liturgies worldwide, across all English-speaking cultures, and the liturgical movement it started was also carried forward by many mainline Protestant and Anglican churches.
• Dynamic Equivalence. Avoiding direct translation from the Latin or Greek, but instead trying to convey meaning in a natural, idiomatic, modern way for the target language.

I personally disagree with some of these goals, but even putting aside my personal disagreements, I think this version of the prayer fails at all of these goals.

• Accessibility to normal English speakers. The line "Save us from the time of trial" seems to be referring to a particular time in the future — perhaps the time when Christ returns — rather than the trials and temptations of everyday life, to which the prayer was originally referring. In fact, I suspect almost all English-speaking Christians would think this line now refers to an apocalyptic time of trial. Doesn't seem very accessible to me.
• Avoiding theological pitfalls. They got rid of the theological problem of "leading into temptation" but added a brand new one: "As we forgive those who sin against us". Firstly, this line implies that it is possible to sin against a human being ("Every sin is chiefly against God" - Thomas Aquinas, ST-II-II 66.6) and, even worse, that human beings have the capacity to forgive sins ("Who can forgive sins but God alone?" - Mark 2:7).
• Ecumenism. The ICEL came up with this translation for use in Roman Catholic liturgy, but it has now been completely removed from use in the same liturgy (and even before, was usually only used in a few dioceses), replaced with a much more direct translation from the Latin Missal. In fact, the only churches still using this terrible translation are mostly Anglican churches like mine.
• Dynamic Equivalence. They half-assed this, replacing the "thy"s and "art"s but leaving in several turns of phrase that clearly come from the Book of Common Prayer ("Hallowed be your name") that don't sound natural or idiomatic in modern English.

I think there's some value in having something beautiful, poetic, or outside the norm in the liturgy. I think this is the value of the Latin liturgy, but the same value can be found in the poetic language of the BCP liturgies. Having something that appears "not of this world", different from the mundane language we use every day, is important to elevate the liturgy and set it apart from the normal day-to-day life of worshippers. The whole idea of "Dynamic Equivalence" robs the liturgy of its distinctiveness. I hope one day my church will put the APBA in the dustbin of history where it belongs.

Ad te levávi ánimam méam: Déus méus in te confido, non erubéscam: neque irrídeant me inimíci mei: étenim univérsi qui te expéctant, non confundéntur.

This Sunday at All Saints Ainslie we were almost pre-warmed up from our rehearsal yesterday (for next week's Carol service). We sang Waters' lovely short anthem I sing of a maiden that is mateless:

I syng of a mayden þat is makeles,

kyng of alle kynges to here sone che ches.

He came also stylle þer his moder was

as dew in aprylle, þat fallyt on þe gras.

Moder & mayden, was neuer non but che –

wel may swych a lady, Godes moder be.

I am starting to organise a group of monthy Evensong singers for next year. If you want to contriubte your voice, please get in touch with me!

Also, as I recently got a collection of Tallis anthems to add to my score collection, I sang through a verse of Why fum'th in sight, the anthem that would, long after its writing, be rediscovered by Ralph Vaughan Williams and inspire his beautiful Fantasia for string orchestra.

I've sketched out a design and begun implementation of a programming language, called Hito. Partly, this is just a programming exercise for me, but I also think the language might fill a niche that is currently unfilled.

Hito (from the Japanese pronunciation of the vaguely lambda-esque character 人, which also means "person"), is designed as a embeddable, lightweight scripting language that is purely functional. In particular, it's designed as an embeddable scripting language for situations where something like Lua even would be overkill. Often, full imperative procedures feel to me too heavy, but a language for quick specification of some calculations, formulas, pipelines or filters would be ideal. An example would be mark calculation formulae for a course gradebook. That said, the language is fairly extensible, so it could in theory be used for much more complicated applications.

I've nearly finished the first prototype implementation, which is written entirely in fairly clean, modern C. Primitive operations are pluggable, just as function pointers supplied to the runtime. It uses a simple mark-and-sweep precise garbage collector and a three-stack abstract machine design for executing the code. It will be dynamically typed, with support for pattern matching and a lightweight kind of algebraic data types, and higher-order functions and closures. The syntax is fairly clean, I think, and designed to be approachable to non-FP people. I have yet to make a proper website, but there is a code repository if you want to poke around.

I have a fairly large collection of anthem books and musical scores for sacred music (see my Church Music Corner), to the point where it has become difficult to actually remember what scores I have and where they might be found. So, I made a small plug-in for forester to make sortable, searchable tables for TSV files, and made a small database of all my anthem books. You can have a look at it here.

I'm increasingly uncomfortable keeping my code, this forest, and many of my papers on GitHub, seeing as they feed data to the dreaded bots, they are owned by Microsoft (who feed data and money to the dreaded bots), and it no longer is as intuitive or useful as it used to be.

So, I'm interested in figuring out an alternative to host all my git repositories. Forester uses sourcehut, which is nice because it's so lightweight and free of the dreaded bots, but I find the interface for it very confusing. Perhaps I just need to get used to it. Does anyone have any other suggestions?

DIGNUS est Agnus qui occísus est, accípere virtútem, et divinitátem, et sapiéntiam, et fortitúdinem, et honórem. Ipsi glória et impérium in sæcula sæculórum.

This Sunday we were very few in numbers and without a director at All Saints Ainslie but we held it together for Isom's King of all ages:

King of all Ages, throned on high,

Yet saviour too of those with faith,

Death at your onslaught died in fear,

And grace triumphant rules supreme.

Risen from death, the heav'nly Christ,

Receives from God the Father's hand,

Power over all created things,

A gift he could not know on Earth.

Then at your coming on the clouds,

With shining strength to be our judge,

Cancel the debt we owe you still,

Give back the glory we have lost.

Glory to you, O Christ our Lord,

Exalted far beyond our sight,

Reigning and forevermore,

with Father and with Paraclete.

I busted out my falsetto for a few bits, but we survived. The Carols and Lessons service is coming up on December 7th, so we have many rehearsals over the next few weeks.

My collection of vintage computers are now safely situated in my new home in Dickson. This week I purchased some new furniture to house some of my most prized machines. At some point I will make a database of everything I've got here in my forest, but here's a photo of some of my lab in the mean time:

I've lived in Canberra for over a year, and yet I never saw the Gang-gang Cockatoo, the ACT's faunal emblem since 1997, despite seeing parrots of all sorts on my walks around the city's various natural areas.

Fortunately, when I was walking on the Dickson bike path today, I saw a couple on a nearby gum-tree, behaving completely oblivious to the city bustle around them.

Dicit Dóminus: Ego cógito cogitatiónes pacis, et non afflictiónis: invocábitis me, et ego exáudiam vos: et redúcam captivitátem vestram de cunctis locis.

This Sunday we were few in numbers at All Saints Ainslie but we sang well for Anna Þorvaldsdottir's Heyr þú oss himnum á, doing our best at the Icelandic pronunciation:

Heyr þú oss himnum á	Hear us in heaven,
hýr vor faðir, börn þín smá,	loving Father, as we, your small children,
lukku oss þar til ljá,	ask for the fortune
lif eilíft þér erfum hjá,	to receive eternal life.
og að þér aldrei flæmumst frá.	We shall not stray from your path.
Þitt ríki þróist hér	May we help your kingdom
það þín stjórn og kristni er,	to grow here on earth.
svo að menn sem flestir,	Following your guidance,
safnist, Guð, til handa þér,	we gather around in your name
fegin yfir því fögnum vér.	and gladly celebrate.
Síst skarta sönglist má,	We cannot make a joyful song
sé þar ekki elskan hjá,	unless we are moved by love.
syngjum þvi þýtt lof þá,	So let us sing our gentle praise
Þér, Guð drottinn, himnum á.	to you, Lord God, in heaven,
Maður rétt kristinn mun þess gá.	as the truly faithful have done.
En þegar aumir vér,	When our poor souls
öndumst burt úr heimi hér,	pass away from this world,
oss tak þá, Guð, að þér	take us God to you,
í þá dýrð, sem aldrei þver.	into your everlasting glory.
Amen, Amen, það eflaust sker.	Amen, Amen, may this be done.

We also are going to be thin on numbers for Christ the King next week, and I will be directing. I welcome any anthem suggestions that aren't too reliant on sopranos in particular.

As I previously mentioned, I am teaching at the ANU Logic Summer School this year, on an introduction to interactive theorem proving using the proof assistant Isabelle. Here's the course blurb as found on the website:

I will also make the course notes available on this forest, as they are completed.

Similar to my theme plugin for Gregorian Chants, I've implemented a simple plugin for syntax highlighted blocks using the Shiki library. Unlike the chant plugin, it doesn't self-host all the required JS but instead loads from a CDN. If this becomes problematic later I will investigate self-hosting it, but it seems that self-hosting Shiki is somewhat complicated.

I didn't use any other syntax-highlighting gizmos for Forester because I plan to write lecture notes for my upcoming course at the LSS and this would require me to support Isabelle code. The advantage of Shiki is that it supports textMate grammars, and Gerwin Klein made one for Isabelle.

Like the chant plugin, it consists of a single drop-in module of JavaScript, some changes to the stylesheet and a macro definition tree. As can be seen below, the results are quite nice:

(If it doesn't display correctly, you may need to clear your browser cache.)

Intret orátio mea in conspéctu tuo: inclína aurem tuam ad precem meam Dómine.

This Sunday I directed our choir at All Saints Ainslie for Purcell's Thou Knowest, Lord:

Thou knowest, Lord, the secrets of our hearts:

Shut not, shut not thy merciful ears unto our prayer,

But spare us, Lord. Spare us, Lord most holy.

O God! O God most mighty! O holy and merciful Saviour,

Thou most worthy judge eternal,

Suffer us not, suffer us not at our last hour,

For any pains of death to fall from thee.

Amen.

We also had a brief meeting yesterday morning to discuss our future plans for the choir. We have some exciting music ahead, and some of us agreed to sing at a special service at Goodwin Retirement Living for the residents there during Advent. Next year at the church, we plan to have semi-regular concerts, and I will also be forming a small group to sing regular Evensong services.

From the 10th to the 19th of October I was travelling, specifically to Singapore to present the results of the ICFP '25 Programming Contest. As seems to almost always happen, the Japanese team Unagi (and another Japanese team, MOYOU) won the contest, using their preferred programming language Rust. Also as in most years, most solutions used SAT encodings, simulated annealing, or other such methods. Some teams did use automata learning (as our reference solution did), but this was uncommon. The writeups page has many more details, including an in-character personal reflection by Adso.

The conference was indeed massive, and it was good to catch up with many folks that I know (such as Gabriele Keller, Christine Rizkallah, Zilin Chen and Michel Steuwer), but I must say that I found few talks or papers that I actually found noteworthy or compelling. Perhaps the most interesting was the few papers and presentations I saw given by Anton Lorenzen. I'm sure this is more a problem with me than with the authors, all of which I'm sure have produced very good work, except of course for the LMPL Workshop which promotes use of the dreaded LLMs in PL research. I studiously avoided attending that, and was pleased to find some likeminded colleagues.

While I love to eat the food in Singapore, I always find the weather almost unbearable. I try to do what locals do, and transit via underground and indoor connections between buildings, but I inevitably end up having to walk for 10–20 minutes outside and end up feeling horribly wet from a mixture of humidity and sweat. Nonetheless, I thank very much Ilya Sergey and the others who organised the event, and arranged for me to travel there and present.

Ego clamávi quóniam exaudísti me, Deus: inclína aurem tuam, et exáudi verba mea: custódi me, Dómine, ut pupíllam óculi: sub umbra alárum tuárum prótege me.

I had just flown back from Singapore, so I wasn't able to be present for All Saints Ainslie singing Tallis' Hear the voice and prayer but I did record myself singing all parts to it a week earlier before I flew out:

Hear the voice and prayer of thy servants,

that they make before thee this day:

That thine eyes may be open towards this house night and day,

Ever towards this place, ever towards this place

Of which thou hast said "My name shall be there".

And when thou hear'st, have mercy on them.

I had just flown into Sydney and coming down with a cold from a nightmare flight, but I was still able to stop by Christ Church St. Laurence for their Solemn High Mass. It was a lovely high church service. I wish we were as liturgically refined in Canberra. The Choir performed most of G.P. da Palestrina's Missa Aeterna Christi Munera, which is based on the eponymous Gregorian Chant melody, and Vaughan William's O Taste and See.

Lætétur cor quæréntium Dóminum: quaérite Dóminum, et confirmámini: quaérite fáciem eius semper.

While I was still recovering from a cold, I sang with our choir at All Saints Ainslie for Anerio's gorgeous piece, Christus Factus Est (although the initial gorgeous passage is very reminiscent of another piece).

Christus factus est pro nobis obédiens	Christ became obedient for us,
usque ad mortem:	Even unto death:
Mortem autem crucis.	Death on the cross.
Propter quod et Deus exaltavit illum	Wherefore God has exalted him,
Et dedit illi nomen quod est super omne nomen.	And given him a name above all other names.

The Anerio was unaccompanied, and we had only piano accompaniment for the other music. Still, we sounded very nice I think.

Gaudeamus omnes in Dómino, diem festum celebrántes sub honóre Sanctórum ómnium: de quorum solemnitáte gaudent Angeli, et colláudant Fílium Dei.

Because this was the dedication feast for All Saints Ainslie, we sang Darke's Communion Service in F Major as well as I Sat Down by John Bairstow, with text taken from the Song of Solomon:

I sat down under his shadow with great delight,

and his fruit was sweet to my taste.

He brought me to the banqueting house, and his banner over me was Love.

I sat down under his shadow.

We also had a small celebration of our choir and sanctuary party at Corroboree park in Ainslie.

We were blessed with a gorgeous sunset to conclude the evening.

I've been reading Umberto Eco's Baudolino recently. It's the story of a man, the eponymous Baudolino, narrating his life story to Niketas Choniates during the Fourth Crusade. Here "story" is used both in the sense of a recounting of events, but also in the sense of a storyteller, a fabulist. Baudolino isn't sure, even to himself, where reality ends and his imagination begins. He is a liar, and in lying he speaks of greater truths.

This novel (which I highly recommend, by the way) represents to a far greater degree the medieval and even classical understanding of truth and history than do contemporary definitions. The ancient Greeks knew that the Iliad or the Odyssey were stories, fabrications of Homer or of countless storytellers before him and since, yet, they referred often to events in those stories as though they actually happened (and, presumably, some of them had), and to characters in those stories as though they actually existed (and, presumably, some of them did). Herodotus, regarded as the first historian, was also prone to elaborate creative embellishment of historical events, usually to paint the Greeks as the good guys and their enemies, usually the Persians, as the bad guys. Herodotus did this openly; his audience expected embellishment and would not have been impressed by a dry recital of facts.

Similarly, up until the late 16th century, even the most learned scholar (and Eco's Baudolino) would speak of the Kingdom of Prester John, a supposedly Nestorian Christian empire far to the East, or possibly South, or anywhere where European Christians had not thoroughly explored. These were fabrications, of course, or at least interpolations based on poorly communicated rumours and legends, but European Christians believed these things as firmly as they believed in the existence of elephants, or of God, or of Julius Caesar, or anything else they didn't observe first-hand. Almost their entire view of the world was based on hearsay, fabrication, and interpolation from available information, and they knew this. They believed it anyway, in a semi-firm way that isn't familiar or comfortable to modern humans. For our ancestors, belief was elastic; for us, it is binary: true or false.

I think our society really began to depart from this more elastic way of thinking in the Enlightenment era: the scientific revolution, the classical insistence on the dichotomy between truth and falsehood, the empirical notion that truth requires evidence, and the positivistic view that a proposition, once shown to be true, is never again false. These ways of thinking have proved enormously beneficial in the area of science and technology, to be sure, but I think this is also responsible in part for many overly rigid belief structures, including religious fundamentalism. It's the result of a pre-Enlightenment cognitive technology (religion) coming into contact with this post-Enlightenment way of thinking. At worst, it leads to ultra-dogmatic religion where religious dogmas are declared to be infallible truths, including fundamentalists who interpret the Bible literally. At best, it leads to pathetic attempts to justify religion on scientific terms, like asking scientists to analyse consecrated Eucharistic hosts to check for human tissue cells.

Just by reading my Church Music Corner, you might get the impression that I am a devout Roman Catholic or Anglo-Catholic Christian. In a sense, that is true (as for which of these I am, that's a topic best left to another time). But my faith is much more akin to that of the medieval scholar than that of a modern empirical scientist. The question of whether the life of Jesus as told in the Gospels actually happened as described is almost irrelevant to me. In fact, as the Gospels do not tell a consistent narrative, one can only conclude that they too are at best interpolations based on hearsay. The Gospel of Luke lists many more parables of Jesus than are listed in the other Gospels: even if they are fabrications of the evangelist, I believe them to be parables of Jesus all the same.

Requiring evidence as a prerequisite for belief is not mistaken — it is just misapplied when it comes to religion. I don't look for proof that my religion is true in the modern, empirical sense. I don't know if it is. At least in some aspect or another, it's almost certainly not. But this question is also irrelevant to me: Truth, in this older sense, is not about evidence but about meaning. My faith is an affirmation not of a proposition but a way of inhabiting the world. Even if I was presented with concrete evidence that the Gospels are complete fabrications and that Jesus never existed (although Occam's razor suggests that he did), my faith would scarcely change. Can I still rightly say then, Credo in unum Deum, as I do each Sunday? All I can say is, I don't feel as though I'm lying.

In voluntáte tua, Dómine, univérsa sunt pósita, et non est qui possit resístere voluntáti tuæ: tu enim fecísti ómnia, cælum et terram, et univérsa quæ cæli ámbitu continéntur: Dóminus universórum tu es.

Vir Dei Francíscus relíquit domum suam, dimísit hereditátem suam, inops et pauper factus est; Dóminus autem assúmpsit eum.

Our choir at All Saints Ainslie was in thin numbers but we lovingly performed Lloyd's View Me, Lord, under my baton (well, hand). It's a lovely poem from Thomas Campion:

View me, Lord, a work of thine.

Shall I then lie drown'd in night?

Might thy grace in me but shine,

I should seem made all of light.

Cleanse me, Lord, that I may kneel

At thine altar, pure and white.

They that once thy mercies feel

gaze no more on Earth's delight.

Worldly joys, like shadows, fade

When the heav'nly light appears;

But the cov'nants thou hast made,

Endless, know not days nor years.

In thy word, Lord, is my trust;

To thy mercies fast I fly.

Though I am but clay and dust,

Yet thy grace can lift me high.

We got many complements after the service and during the rehearsal.

When I lived in Edinburgh my "commute" consisted of a 10 minute walk through the lovely Meadows parkland to get from my apartment to the Informatics Forum. Sometimes I'd have to cross the dreaded North Bridge or the crowded Nicolson street, and I would always find myself feeling overwhelmed and stressed. But, the walk through the Meadows was always healing — or, failing that, it never added to my stress.

When I moved to Canbera, I first lived in Braddon. Like at Edinburgh, or indeed my time at UNSW Sydney, my commute was just a 10–15 minute walk. Yet, unlike at Edinburgh, I would often find the walk stress-inducing.

Since I've moved to Dickson, my commutes have gotten much longer — a 40–45 minute walk from my home along a bike path through the Lyneham wetlands and other beautiful natural parkland. Similarly, the walk from my home to my church is slightly longer, but significantly quieter, following bike paths and sleepy suburban streets. This walk is significantly more mentally healing to me than the shorter commute I had before, and helps me to relieve stress rather than accumulate it.

The main difference is simple: The walk this time passes through mostly parkland, and, for the most part, is not along a road. The noisy cars and, annoyingly common in Canberra, roaring motorbikes of the city traffic are distant, usually inaudible, and in their place I have some stunning natural landscapes and many colourful parrots to greet on my walk to work.

I think car-centric cities are one of the worst mistakes humanity has made in terms of societal engineering. I hate cars. Please get rid of all the cars.

In nómine Dómini omne genu flectátur, cæléstium, terréstrium et infernórum: quia Dóminus factus obédiens usque ad mortem, mortem autem crucis: ídeo Dóminus Iesus Christus in glória est Dei Patris.

Omnia quæ fecísti nobis, Dómine, in vero iudício fecísti, quia peccávimus tibi, et mandátis tuis non obedívimus: sed da glóriam nómini tuo, et fac nobíscum secúndum multitúdinem misericórdiæ tuæ.

I filled in as director of our choir at All Saints Ainslie today for our performance of Dubois' Ave Maria. I am getting more comfortable conducting us. I will be conducting again for next week's service as well.

Ave María, gratia plena, Dóminus tecum.	Hail Mary, full of grace, the Lord is with thee.
Benedícta tu in muliéribus et benedíctus fructus ventris tui, Jesus.	Blessed art thou among women, and blessed is the fruit of your womb, Jesus.
Sancta María, mater Dei, ora pro nobis peccatóribus,	Holy Mary, mother of God, pray for us sinners,
Nunc et in hora mortis nostræ. Amen.	Now and at the hour of our death. Amen.

I think this week's service went really well. Congratulations to all involved!

I'm no longer attending Evensongs at St. Paul's or St. John's because it's now too far from my home in Dickson. Hopefully we can start some more frequent Evensong services at All Saints.

Last week I attended the meeting of IFIP Working Group 2.1: Algorithmic Languages and Calculi in Viana do Castelo, Portugal. I think all members and observers agreed that it was a good meeting, with (perhaps overly) abundant food and good company. Thanks in particular to José Nuno Oliveira for organising the meeting and to Peter Höfner for serving as chair of WG2.1 for the last six years.

Because this was my third meeting as an observer, I was eligible to be selected as an ongoing member of the group, and I'm happy to say that I was invited to become a member at the conclusion of this meeting.

I presented some new work my student Rayhana and I did with Rob van Glabbeek, classifying monitorability classes topologically.

This was the sequel of sorts to my prior WG2.1 talk on LTL properties within finite time, which was in turn presenting work from our EXPRESS/SOS paper last year. The topological connection was realised thanks to Nicolas Wu, also a WG2.1 member, who pointed out in the Canberra meeting that the work I was presenting had distinct notes of domain theory. The topological connection was more that of Alpern and Schneider than Scott, but that was the spark that drove this later work, which will hopefully be included in our forthcoming Information and Computation paper.

The excursion of the meeting included several stops, including two interesting Viana museums, an archaelogical site on the nearby mountaintop, and a memorable trip to Camarido Beach, at the northernmost tip of Portugal, with Spanish Galicia just to the north along the road from Portugal to Santiago de Compostela.

After the meeting had formally concluded, Oleg Kiselyov, Fritz Henglein, Matija Pretnar, Thomas Sewell, Ningning Xie and I climbed to Santuario de Santa Luzia. We took the arduous stairs rather than the funicular, as Matija's wife had forbidden him from Portuguese funiculars after the recent Ascensor da Glória derailment, which led to me overdoing it and nearly fainting, but in recompense Matija bought me a beer at the top of the mountain which made it (mostly) worth it!

Hopefully I can make it to the next meeting in Estonia next year!

While I was flying to Portugal, the ICFP '25 Programming Contest was ongoing. Despite my anxieties about exorbitant AWS bills and crippling server bugs, the contest went relatively smoothly. Jack Stodart helped out in parts where I was unavaiable. I did have to fix some minor bugs here and there, mostly in the first hour of the contest (although I also had to fix a tricky bug in the post-lightning round problems using the flaky WiFi at Lisbon airport), but the server ended up holding up very well, and the cost of the various AWS services I used (primarily DynamoDB and Lambda) was only a total of about $20 USD.

My task description, post-lightning round addendum and reflective afterword were all themed around Umberto Eco's The Name of the Rose, and I put a great effort into the typesetting of these three documents. It was nice that many contestants picked up on the theming, and appreciated the typesetting. For promotional graphics, I posted images of the Seven Trumpets from the medieval Cloister Apocalypse, an illustrated manuscript of the Book of Revelation. One contestant posted AI-produced remixes of these timeless masterpieces of medieval illumination, which had my finger hovering over the ban button, but I was able to separate my personal revulsion of LLMs from my role as competition organiser. Besides, it would have been hypocritical.

One other "contestant" seemed to be participating simply to flame the organisers. While they were eventually banned from the Discord (thanks Alperen!), it was a big downer right at the start of the competition. This one individual aside, it seems that the contestants broadly enjoyed the competition and had fun solving it.

While it was interesting reading the write-ups and seeing the various approaches to the problems, I came away from this contest with the distinct impression that the ICFP community and the ICFP contest community are, for the most part, non-overlapping. This, combined with the immense stress it puts on organisers, leads me to wonder if the ICFP contest might be better off being organised by its own community, rather than the ICFP one. I'm not sure what benefit the connection to ICFP or ACM has to the contest community, if any, and I'm fairly sure there are no benefits in the other direction. I no longer think severing the ICFP connection would be tantamount to discontinuing the contest, because the contest community surely seems to have enough critical mass to be self-sustaining. Perhaps I will raise this with the ICFP steering committee.

The ANU Logic Summer School is back again this year, and this time I feature on the program. I will be teaching an Introduction to Interactive Theorem Proving using Isabelle/HOL. The timetable is tentative but it looks like I will be teaching it over the final two days of the first week, with one two-hour and one one-hour lecture per day. This means it will be quite a packed programme, but I will do my best.

It's my hope that I can figure out a nice way to include Isabelle code in Forester trees, so that I can make my lecture notes with Forester. But this may be difficult for a variety of technical reasons, so in the worst case it will be a bunch of Isabelle theory files with comments.

My introduction will hopefully tie in to Chelsea Edmonds' teaching Hoare logic and rely/guarantee reasoning in Isabelle over the second week.

If you or your students have an interest in logic or verification, please consider sending your students! We also have some limited scholarships available.

Both Peter Höfner and I enjoyed Tom Schrijvers' talk at the IFIP WG2.1 Meeting #83 answering a challenge from Bruno C. d. S. Oliveira: to stepwise derive his QuickSub efficient iso-recursive subtype checking algorithm from the exponential-time Amber rules of Luca Cardelli's \mathcal {F}_{<}. Impressively, Tom and his student were able to get there, and it's certainly nice to have such a neat justification of QuickSub's correctness, but I did experience some mild irritation: The calculation was done with a very specific goal in mind — namely the QuickSub algorithm — and so several steps in the proof were, in a sense, "goal-motivated". If we didn't know the QuickSub algorithm in advance, many steps would have had no intuition behind them at all. Another member of the group called such steps "eureka steps".

It led me to wonder about the myriad of possible choices available at any given step in that refinement. Why do we choose this algorithm? If I recall some of the classic works on program calculation from Richard Bird or Carroll Morgan, the algorithms we end up with proceed from a series of calculations, each of which makes sense in isolation. You can read the derivation from beginning to end and each step feels like it's improving the algorithm in some way. The process feels entirely natural. Whereas here, these "eureka steps" mean that I need to look much further ahead to find the motivation for the transformation being performed.

I encountered a similar feeling when my student Xin Lu raised Concurrent Incorrectness Separation Logic for discussion with me and Peter Höfner. Incorrectness Logic is, in a nutshell, a logic for showing the presence of bugs rather than their absence. One of its nice qualities is that, like its almost-dual Hoare logic, it offers a relatively calculational way to approach program (in)correctness, where each proof step follows naturally from the structure of the program and the assertions within it. Unfortunately, Concurrent Incorrectness Separation Logic doesn't quite preserve this property when moving to a concurrent setting. To prove the existence of concurrency bugs like races, each thread's local assertions build a history of writes and lock actions, and then, in the assertion after the potential race, a "eureka step" comes in which points out the problematic interleaving of these histories that exhibits the race condition. Proving the presence of this bug required first knowing that the bug exists and how it can arise, and then doing the same "goal-motivated" reasoning that we saw in Tom's talk. This seems to me quite dissatisfying. Is there a more genuinely calculational approach here? I suspect concurrency makes things fundamentally more difficult, but I think we should nonetheless strive for the elimination of these "eureka steps" even if it's not always possible to do so.

Salus pópuli ego sum, dicit Dóminus: de quacúmque tribulatióne clamáverint ad me, exáudiam eos: et ero illórum Dóminus in perpétuum.

Protexísti me Deus a convéntu malignántium, allelúia: a multitúdine operántium iniquitátem, allelúia, allelúia.

Venite benedícti Patris mei, percípite regnum, allelúia: quod vobis parátum est aborigine mundi, allelúia, allelúia, allelúia.

Our choir at All Saints Ainslie was in relatively full numbers, except that we had zero altos and no director. I filled in as director and appointed a few of our singers to cover the alto part for one of my favourite motets, Byrd's Ave Verum Corpus. We were originally set to sing Lloyd's Benedicta sit (for which I can find no recording), but the substitution was made to a more familiar anthem due to our shortage of altos and a director.

Ave verum corpus natum de María Vírgine,	Hail, true body, born of the Virgin Mary,
Vere passum immolátum in cruce pro hómine,	True suffering, sacrificed on the cross for Man,
Cuius latus perforátum unda fluxit sánguine,	From whose pierced side flowed waves of blood,
Esto nobis prægustátum in mortis exámine.	Be for us a foretaste in death's trial.
O dulcis, O pie, O Iesu fili Maríæ,	O sweet! O blessed! O Jesus, son of Mary,
Miserére mei, miserére mei, miserére mei.	Have mercy on me, have mercy on me, have mercy on me.

We sang at the front of the church today (as we had no organ) which I think gave a better acoustic. We got many complements after the service.

Miserére mihi Dómine, quóniam ad te clamávi tota die: quia tu Dómine suávis ac mitis es, et copiósus in misericórdia ómnibus invocántibus te.

Today our choir at All Saints Ainslie were about two to a part for Palestrina's well-known Sicut Cervus:

Sicut cervus desíderat ad fontes aquárum:	Like as the hart desireth the waterbrooks:
ita desíderat ánima mea ad te, Deus.	So longeth my soul after thee, O God.

I finished the first 5 weeks of teaching for Programming as Problem Solving this week, which marks the point in the course where I hand over lecturing duties to Ranald Clouston. Tomorrow I will be up early to invigilate the mid-term exam, which I spent the last week setting up. I think it will be sufficiently brutal to give a shock to those students who have not sufficiently engaged, while still being fair and achievable for that handful of students who are attending classes and strongly engaging with the course.

I was absolutely mortified in the first lecture of my final week when only two students (out of almost 120) showed up. I later found out that my handful of regular attendees had a maths exam the same time, which lessened the impact somewhat.

I have no doubt that most of those who actually attend my lectures will do well. They are very on the ball, and they seem to enjoy my lectures. One asked what other subjects I teach, and another gave me a delicious carrot cake after my final lecture, which was a very touching gesture!

I've been putting the finishing touches on the server for the ICFP '25 Programming Contest, which I am organising. With Jack Stodart and Alex Mirrlees-Black we will put it through a test run this week, if I can find the time.

I wrote the server in Kotlin and used AWS Lambda, AWS DynamoDB and other Amazon Web Services. The point of this approach was so that I wouldn't have to worry about scalability, but I am slightly nervous that the costs will be much higher than I expected. I guess I'll cross that bridge when I come to it.

I must say that the state of documentation for AWS is simply atrocious. On one occasion, in desperation to find some answers to what I thought were simple queries, I turned to the dreaded bots for help. They gave me incorrect answers, of course, but I was at least able to Kagi search my way to success based on their answer. Still, I feel like I need to go to confession and receive absolution for interacting at all with those infernal machines.

Another concern is that I am flying from Sydney to Portugal while the contest will be going on. I'm hoping Jack will be able to monitor things without me, but mostly I'm going on faith that nothing will explode.

I'm theming this year's contest around one of my all-time favourite novels, Umberto Eco's The Name of the Rose. Some of the folks on our Discord channel have been enjoying that.

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!

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 Anton Brucker's classic Locus Iste:

Locus iste a Deo factus est.	This place is made by God,
Inaestimábile sacraméntum,	A priceless sacrament,
Irreprehensíbilis est.	Beyond reproach.
Locus iste a Deo factus est.	This place is made by God.