Two weeks ago I went to Glasgow to attend the Scottish Programming Language and Verification summer school 2024, or SPLV24 for short. My industry ticket was financed by The PHP Foundation.
Monday and Tuesday morning were composed of Conor McBride talking about Type Theory and Chris Heunen's Category Theory course.
Conor's lecturing style made me think I forgot how to take lecture notes, but it feels more like a consequence of their slightly chaotic way of lecturing rather than anything else (or so I want to believe).
They did assume some fundamentals about logic and how a typing judgement is structured, but I mostly managed to follow what was going on in their definition of a bidirectional simply typed lambda calculus. The final hour was dedicated to looking through an implementation of such a type system in Agda.
Chris Heunen's couse was an excellent speedrun through Category Theory. It was nice to mostly go through big picture ideas rather than getting bogged down with individual proofs. If I have the motivation I might typeset my notes/Chris's slides in Typst.
Jean-Marie Madiot's Separation Logic course was quite dense, being an emergency substitution based on a longer syllabus after Lindsey Kuper had to cancel due to COVID. Even though I didn't grasp all the content, the course gave me a good overview of what separation logic is, what it can do, a quick look at Iris (a framework for separation logic written in Coq), and that it should in theory be possible to formally model PHP with separation logic.
For the specialised courses I mostly attended the second track: after initially going to Kathrin Stark's "Mechanization of Binders" lecture I quickly realized that I had none of the required background, so I swapped to Jules Hedges's "Applied Category Theory" lectures instead. As I missed the first lecture, I was catching this mid-flight without the best understanding of string-diagrams. However, it still felt approachable. The main ideas I took from that course are that flowcharts can be viewed as string diagrams, finally understanding what Lenses are (after having heard this term quite a bit), and a rough overview of how Quantum Computing actually works via ZX-formalism.
Andrés Goens's "Protocol Verification" course was fascinating and taught me the basics of what a Label Transition System (LTS) and Linear Temporal Logic (LTL) are. He also showed us how to use Promela to write a protocol in a C-like language and how Spin is used to verify the model generated by Promela. It turns out Promela/Spin can check very large state spaces rapidly, which might not be easily done via a usual proof checker, as demonstrated on a real world example of a piece of hardware utilizing two different CPU architectures together with a common memory. Some interesting ideas that came out when talking with Andrés were:
Sam Lindley's "Effects and Handlers" course felt like the most practical, as it talked about how one can encode effects, such as choice, yield, fail, random, and display into a type system and use an "effect handler function" to consume such an effect which decides how to dispatch a resumption.
For example computationMightFail(T $v): S!fail indicates that computationMightFail is a function that takes in a value of type T returns a value of type S, but also that this function may cause the effect fail.
The clear advantage of effects over monadic types is that fn(T $v): S is still a subtype of the function type fn (T $v): S!effect whereas it is not a subtype of fn(T $v): Maybe<S>.
Moreover, PHP already has different, non-unified, ways to handle various effects: try-catch blocks to handle exceptions, setting an error handler to handle E_WARNINGs and co, capturing output via the ob_* functions, etc.
The other nice outcome when effects are a core feature of a language is that users can create their own!
Sam also went into ways to implement such effect types via row-types (and it looks like using Leijen-style row polymorphism is better), and different ways one can define effect handlers such as "deep", "shallow", or a hybrid of both named "sheep", which is what they ended up implementing for WASM FX.
Having the lightning talks on Monday and Tuesday evening before the excursion on Wednesday was also a good idea on the part of the organizers, as after hearing from Christopher Lam about language verifications, I could talk to him during the excursion and get his opinion on what might be needed to implement this for PHP. It was also cool to hear Wenhao Tang talk about their paper ([2407.11816] Modal Effect Types) that has been making the rounds in the PL community. Another fun talk was the one from Cass Alexandru talking about their paper formalising sorting algorithms.
It was also very nice to talk to a variety of people about their research or what they do in industry, from session types, quantum computing, formalisation, working on Kotlin, and more!
A lot of people asked me about Hacklang and how it relates to PHP nowadays, so maybe I (or someone else!) should write about the history of both and how they intertwine?
Finally, communication and organisation were done via Zulip, which I had known about for a while because the Lean community uses it too. I didn't create an account to participate in the Lean Zulip when I was at Imperial because I didn't want to use yet another communication tool. One clear advantage of Zulip over Slack and Discord is that messages can be publicly listed so that everyone can read them, even without an account. Which makes it feel more like a modern take on email rather than yet another messaging app, it being open source (like email) may also be part of the reason I feel this way. The biggest downside is the interface. The browser app on a desktop is mostly fine after a bit of trial an error, whereas the mobile app is utterly confusing and even after using it for a week I still get lost in it.
Overall, I enjoyed SPLV24 a lot, learned a bunch, and came back with many ideas - the main ones being how to add effect types (possibly by starting with static analysis tools first, might require nudging Ondřej Mirtes) and different ways for formalising PHP and verifying PHP code.
Hopefully I'll be able to attend again!