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.