This week felt quite productive. The Logic Summer School has now finished, and my PhD student at University of Edinburgh, Rayhana Amjad, has now embarked back to the UK. My course (Interactive theorem proving) was only for the first week, so I had some time to get work done this week. Peter Höfner and I finally finished a mammoth proof in Isabelle that matrices over a Kleene algebra are themselves a Kleene algebra, a proof that's important for Dexter Kozen's completeness result for Kleene algebras. This required some novel proof engineering, and some constructions to make the proof go though that we think Dexter may have missed in his pen-and-paper proof. I may write up my thoughts this coming week, but it's also possible that you might have to wait for a paper. Rayhana Amjad and I also sketched out some future directions for our work, which is quite exciting.
A picturesque cloudy Canberra evening.
Web Components are confusing; bugs fixed. [loc-002N]
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.
