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.
Holbert-NG status: pluggable terms and tangled [loc-0040]
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.
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.
