What I learnt at ICFP/SPLASH 2025 about OCaml, Hazel and FP / Oct 2025

(This is part 5 of my ICFP25 series: see also 1. Chairing PROPL25, 2. OxCaml tutorial, 3. OCaml 5 with Jane Street and Docker, 4. post-POSIX IO

In addition to giving a bunch of talks about Docker, post-POSIX and planetary computing, the greatest fun at a huge conference like ICFP and SPLASH is seeing talks given by my students (they grow up so fast!) and collaborators, and generally floating around random talks trying to deceipher ancient Greek lambdas floating on a projector.

Hazel live programming and type level debugging

I've been wanting to try to do something with Hazel ever since Cyrus Omar showed it to me at last year's PROPL. Max Carroll picked up the idea of doing gradual type-level debugging for his Part II undergraduate project at the Computer Lab. He not only aced his project, but wrote up a paper for the HATRA workshop:

We explore how to provide programmers with an interactive interface for explaining the process by which static types and dynamic casts are derived, with the goal of improving the debugging of static and dynamic type errors.

To this end, we define mathematical foundations for a decomposable highlighting system within a bidirectional system, and show how these can be propagated through dynamic types in a cast system. Our prototype implementation in the gradually typed Hazel language includes a web-based user interface, through which we highlight the importance of type level debugging. -- Decomposable Type Highlighting for Bidirectional Type and Cast Systems, Carroll 2025

Max Carroll delivered a fantastic first conference talk, complete with a live demo demonstrating type-level debugging in action; give it a watch if you're interested in live programming!

One issue we had during this project was finding a decent corpus of functional code with errors to use to test out Max's debugger. Hazel's a pretty young language, and finding a large codebase is difficult, let alone a bunch of code with errors. Patrick Ferris decided to accelerate this process by building a hazel_of_ocaml and presenting this work at the TyDE workshop.

With Patrick's transpiler, we grabbed Eric Seidel's corpus of ill-typed OCaml that he built for his research on dynamic witnesses for static type errors. Max successfully used this translated corpus to build his type-level debugger, and is planning to continue to work on this in his Part III project this year.

Three Steps for OCaml to Crest the AI Humps

I've been spending a lot of time with my friend Claude recently, and so have Sadiq Jaffer and Jon Ludlam. We wrote up our experiences with interfacing OCaml with coding agents, and Sadiq presented it to an interactive crowd at the OCaml Workshop.

Aside from the very sensible guidance on MCP and tools, I discovered a couple of things from this work:

• Sadiq Jaffer found terminal-bench and added an OCaml GC debugging task. This has the effect of getting the frontier AI labs to point their mega training tasks at OCaml-related problems, thus making a rising tide for everyone! And looking at the history of the task, other labs are raising the timeout on Sadiq's task, meaning that fixing bugs in the OCaml GC is right at the top end of difficulty. Let's get more problems into terminal-bench!
• It also surprised me just how good the Qwen coder models are on simple OCaml tasks. Local models are fairly far behind Claude's, but the gap is closing as the innovation moves to the agentic context management. I'm excited to see Thibaut Mattio's work on Spice (see his FunOCaml talk) as that combines these local models with OCaml-specific context management.

Formally verified garbage collector for OCaml

Sheera Shamsu gave a fantastic talk on building a formally specified garbage collector for OCaml to a very crowded room! This was rather topical given our musings on multiple runtimes in the shift from OCaml 4 to 5.

[...] we propose a strategy for crafting a correct, proof-oriented GC from scratch, designed to evolve over time with additional language features. Our approach neatly separates abstract GC correctness from OCaml-specific GC correctness, offering the ability to integrate further GC optimizations, while preserving core abstract GC correctness. As an initial step to demonstrate the viability of our approach, we have developed a verified stop-the-world mark-and- sweep GC for OCaml. The approach is mechanized in Fstar and its low-level subset Lowstar. -- A Mechanically Verified Garbage Collector for OCaml, Shamsu et al 2025

Chatting to KC Sivaramakrishnan afterwards, it seems that there's interest in shifting to Lean from Fstar to investigate if the ergonomics of the proofs are better. But as baselines go, the mechanically verified collector always beat the conservative Boehmm-GC, which means it's no worse than the current more conservative choice. That's good work!

Haskell and OCaml, the Twain Shall Meet?

Most "wonderful ICFP experiences" usually include crossing the lines to go hang out with other language communities.

Back in 2014, I stayed up all night before my keynote to the Haskell Symposium trying to encode OCaml functors as Haskell typeclasses and even got help on stage from friendly Haskellers. This year, Richard Eisenberg was my absolute highlight with a superb session on what he's learnt from being the rare breed of someone steeped deeply both in Haskell and OCaml. The room was so packed for this talk that they had to create an overflow room streaming it in the corridors!

Richard talked about his experiences with being both an OCaml and Haskeller, and went through a series of examples illustrating the differences between the two. He didn't get very far before the audience got involved, with both Haskellers and OCamlers putting their 2c in! For that reason, the stream recording might not work so well.

It's worth watching the talk rather than me going through each of his examples, but I did have a long morning coffee with Simon Peyton Jones when I got back to Cambridge about what the essential difference is between OCaml and Haskell. Laziness seems like a detail, but purity is absolutely key; it percolates through every other design decision (like ordering of variables, or module generativity, and so on) since side-effects lurk everywhere in OCaml.

I think it's really important to have these cross-community in-person moments. One call to action in Richard's talk was for us to consider having a unified "Haskell/ML Symposium" where long-form research papers could be shared, with shorter language-specific workshops. One audience member asked why this couldn't just be the ML Workshop, and Richard promptly pointed out that it has "Higher-order, Typed, Inferred, Strict" in the title! Just excising one word might unify two communities long split for decades...

Aside from language matters, I think it would be a good idea to bring more of the functional programming community together more often outside of the "main ICFP track" (which is high pressure and quite squeezed for time with little discussion outside the corridor tracks). I really miss CUFP, since for a decade this was where the functional hackers would all meet up towards the tail end of the main conference. This year however, the workshops were run in parallel with the main ICFP and OOPSLA, which I think sadly diluted the community bonding a bit.

I got Shriram'ed about our Cambridge teaching

Speaking of teaching, noone in the world can school me better than Shriram Krishnamurthi when it comes to matters of computer science pedagogy. I grabbed him at the lunch break and asked him for advice on our upcoming reform of the Cambridge Computer Science Tripos (I teach the first course). His opinions were legion, and he kindly gave me a quick spin around what they are working on at Brown.

The SMoL (Standard Model of Languages) has a nice web interface and quiz, just like the one he helped on for our OxCaml tutorial. SMoL is deliberately language agnostic:

• If students master SMoL, they have a good handle on the core of several of these languages.
• Students may find it easier to port their knowledge between languages: instead of being lost in a sea of different syntax, they can find familiar signposts in the common semantic features. This may also make it easier to learn new languages.
• The differences between the languages are thrown into sharper contrast.
• Students can see that, by going beyond syntax, there are several big semantic ideas that underlie all these languages, many of which we consider “best practices” in programming language design. -- Fixing Standard Misconceptions about Program Behaviour, 2024

Much like Richard Eisenberg's talk on Haskell/OCaml, the SMoL tutor shows multiple languages for the same problem, rotating across Python, Scala, JavaScript and so on. I like this idea a lot for our Foundations of CS course, as I've been considering rotating in Hazel into the mix to ease the syntactic shock of using OCaml. SMoL takes this concept much further, and is backed by serious user studies on students.

I also really liked the PyRet approach of starting to teach using tables as a core datastructure, and not lists or arrays. However, I'll need to think hard about how this teaching model would work under Cambridge's quirky supervision model.

This is on my queue to work on over the winter, while Jon Ludlam kindly covers my undergraduate lectures for this year while I'm on sabbatical! On my reading list from chatting to him:

• Data-Centricity: A Challenge and Opportunity for Computing Education, CACM 2025.
• Modeling as a core component of structuring data, Konold 2017.

Deterministic WASM

Webassembly has also gone a long way since I last looked into it. I had a long chat with Phillipa Gardner on the nature hike to learn about her work on SpecTec, which is a single source-of-truth DSL that describes both the Wasm specification and the artefacts like the interpreter.

After that, Ben Titzer told me about WALI which is an alternative approach to WASI that simply exposes Linux kernel interfaces straight to the wasm runtime. I'm rather amenable to this given my case for shared memory IO earlier in the week at VMIL, so this is now on my list of things to investigate! KC Sivaramakrishnan, Chris Casinghino and I discussed what an OxCaml wasm unikernel might look like (a lot of buzzwords, I know), and we are pretty close to OxCaml making it possible to write runtimes using itself -- it just needs support for "external memory", which is a topic the Jane Street interns worked on over their summer projects.

Wrapup thoughts on Singapore

Overall, I had a brilliant -- if exhausting! -- week in ICFP in Singapore. I loved the city, I loved the vibes around the conference, and it was totally worth the trip. Huge thanks to Ilya Sergey and the organising team for making this happen!

(This is part 5 of my ICFP25 series: see also 1. Chairing PROPL25, 2. OxCaml tutorial, 3. OCaml 5 with Jane Street and Docker, 4. post-POSIX IO