# What I learnt at ICFP/SPLASH 2025 about OCaml, Hazel and FP
*2025-10-09 — note*
This is part 5 of a [series](https://anil.recoil.org/notes/icfp25) of posts[^1] about ICFP 2025.
In addition to giving a bunch of talks about
[Docker](https://anil.recoil.org/notes/icfp25-ocaml5-js-docker), [post-POSIX](https://anil.recoil.org/notes/icfp25-post-posix) and
[planetary computing](https://anil.recoil.org/notes/icfp25-propl), 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](https://hazel.org) ever
since [Cyrus Omar](https://web.eecs.umich.edu/~comar/) showed it to me at [last year's PROPL](https://watch.eeg.cl.cam.ac.uk/w/3nGExywoVm6XFRBA2zYxSL).
[Max Carroll](https://maxcarroll0.github.io/blog/) picked up the idea of doing [gradual type-level debugging](https://anil.recoil.org/ideas/gradual-type-error-debugging) for his Part II undergraduate project
at the Computer Lab. He not only aced his project, but wrote up a
[paper](https://maxcarroll0.github.io/assets/papers/Carroll-Decomposable_Type_Highlighting.pdf)
for the [HATRA](https://conf.researchr.org/home/icfp-splash-2025/hatra-2025)
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](https://maxcarroll0.github.io/assets/papers/Carroll-Decomposable_Type_Highlighting.pdf), Carroll 2025
Max Carroll presenting his work on gradual type-level debugging in Hazel
[Max Carroll](https://maxcarroll0.github.io/blog/) 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](https://patrick.sirref.org) decided to accelerate this process by building a
[hazel\_of\_ocaml](https://github.com/patricoferris/hazel_of_ocaml) and
presenting this work at the [TyDE workshop](https://conf.researchr.org/home/icfp-splash-2025/tyde-2025#program).
Patrick Ferris presents Hazel-of-OCaml at TyDE 2025
With Patrick's transpiler, we grabbed [Eric Seidel](https://eric.seidel.io/)'s
corpus of [ill-typed OCaml](https://zenodo.org/records/806814) that he built
for his research on [dynamic witnesses for static type
errors](https://dl.acm.org/doi/10.1145/2951913.2951915). 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](https://anil.recoil.org/notes/claude-copilot-sandbox) recently, and so have [Sadiq Jaffer](https://toao.com) and
[Jon Ludlam](https://jon.recoil.org). We [wrote up](https://anil.recoil.org/papers/2025-ocaml-ai) our experiences with interfacing
OCaml with coding agents, and Sadiq [presented it](https://youtu.be/Xh5PNe0SxDY?t=24042) to an interactive crowd at the [OCaml Workshop](https://conf.researchr.org/home/icfp-splash-2025/ocaml-2025).
Sadiq couldnt resist a good pun for his OCaml Workshop talk
Aside from the very sensible
[guidance](https://jon.recoil.org/blog/2025/08/ocaml-lsp-mcp.html) on MCP and
tools, I discovered a couple of things from this work:
- [Sadiq Jaffer](https://toao.com) found [terminal-bench](https://www.tbench.ai/) and added an [OCaml GC debugging task](https://toao.com/blog/gc-debug-terminal-bench). 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](https://github.com/laude-institute/terminal-bench/commits/main/tasks/fix-ocaml-gc), 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](https://qwen.ai/home) models are [on simple OCaml tasks](https://toao.com/blog/ocaml-local-code-models). 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](https://github.com/tmattio)'s work on [Spice](https://getspice.dev/) (see his [FunOCaml talk](https://youtu.be/e8Dkj47nxbg?t=99)) as that combines these local models with OCaml-specific context management.
## Formally verified garbage collector for OCaml
Sheera Shamsu gave a fantastic [talk](https://youtu.be/Xh5PNe0SxDY?t=4364) on building a formally
specified garbage collector for OCaml to a very crowded room! This was rather
topical given our [musings on multiple runtimes](https://anil.recoil.org/notes/icfp25-ocaml5-js-docker) in
the shift from OCaml 4 to 5.
Sheera Shamsu on a mechanically verified GC for OCaml
> \[...\] 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](https://link.springer.com/article/10.1007/s10817-025-09721-0), Shamsu et al 2025
Chatting to [KC Sivaramakrishnan](https://kcsrk.info) 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\!
A full room for verified GCs!
## 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](https://anil.recoil.org/videos/ed84b2eb-1b93-4dc3-b746-63a4af13d4ea) 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](https://richarde.dev/) was my absolute
highlight with a [superb session](https://youtu.be/IlQQElKaFvM?t=13184) 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 Eisenberg setting up in a crowded room for his keynote
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](https://simon.peytonjones.org/) 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.
Jane Street had a fun 'corridor track' where they contrasted Haskell and OCaml to passerbys as well, including an unfortunate wedding party that happened to be on the same floor as us.
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](https://conf.researchr.org/home/icfp-splash-2025/mlsymposium-2025#event-overview), 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](https://cufp.org), 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.
KC is the other person who's done both OCaml and Haskell hacking, so it was kind of adorable to see him sitting beside SPJ during the talk!
## I got Shriram'ed about our Cambridge teaching
Speaking of teaching, noone in the world can school me better than [Shriram Krishnamurthi](https://cs.brown.edu/~sk/) 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](https://anil.recoil.org/notes/focs)). 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](https://blog.brownplt.org/2024/04/12/behavior-misconceptions.html) and quiz, just like the one he helped on for our [OxCaml tutorial](https://anil.recoil.org/notes/icfp25-oxcaml). 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](https://blog.brownplt.org/2024/04/12/behavior-misconceptions.html), 2024
Much like [Richard Eisenberg](https://richarde.dev/)'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](https://hazel.org) into the mix to ease the
syntactic shock of using OCaml. SMoL takes this concept much further, and is
backed by serious [user studies](https://cs.brown.edu/~sk/Publications/Papers/Published/) on students.
I also really liked the [Pyret](https://pyret.org/) 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](https://www.undergraduate.study.cam.ac.uk/supervisions-and-assessment).
This is on my queue to work on over the winter, while [Jon Ludlam](https://jon.recoil.org) kindly [covers](https://jon.recoil.org/blog/2025/09/giving-hub-cl-an-upgrade.html) my undergraduate [lectures](https://www.cl.cam.ac.uk/teaching/2526/FoundsCS/) 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](https://cacm.acm.org/opinion/data-centricity/), CACM 2025.
- [Modeling as a core component of structuring data](https://iase-pub.org/ojs/SERJ/article/view/190/95), Konold 2017.
Not a bracket out of place when Shriram is demoing PyRet!
## Deterministic WASM
Webassembly has also gone a long way since I [last looked](https://anil.recoil.org/notes/wasm-on-exotic-targets) into it. I had a long chat with [Phillipa Gardner](https://www.doc.ic.ac.uk/~pg/) on the
[nature hike](https://bsky.app/profile/ningkeli.bsky.social/post/3m2y4ncoiae2n)
to learn about her work on [SpecTec](https://dl.acm.org/doi/10.1145/3656440),
which is a single source-of-truth DSL that describes both the
[Wasm](https://webassembly.org) specification _and_ the artefacts like the
interpreter.
After that, [Ben Titzer](https://s3d.cmu.edu/people/core-faculty/titzer-ben.html) told me about [WALI](https://arxiv.org/abs/2312.03858) which is an alternative approach to [WASI](https://wasi.dev/) that simply exposes Linux kernel interfaces straight to the wasm runtime. I'm rather amenable to this given my [case for shared memory IO](https://anil.recoil.org/notes/icfp25-post-posix) earlier in the week at VMIL, so this is now on my list of things to investigate! [KC Sivaramakrishnan](https://kcsrk.info), [Chris Casinghino](https://tyconmismatch.com/code.html) and I discussed what an [OxCaml](https://anil.recoil.org/notes/icfp25-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](https://blog.janestreet.com/wrought-2025/#ref-counted-objects-in-shared-memory) 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\!
The vegetarian food was amazing and my diet is in tatters.The coffee was 'ok'; I wonder what Satnam Singh thought about it!The views were spectacular. Singaporean architecture is ridiculous.
*10th Oct 2025: Typo fixes spotted by Shriram.*
[^1]: See also in the [ICFP25](https://anil.recoil.org/notes/icfp25) series: [chairing PROPL25](https://anil.recoil.org/notes/icfp25-propl), the [OxCaml tutorial](https://anil.recoil.org/notes/icfp25-oxcaml), [multicore at Jane Street and Docker](https://anil.recoil.org/notes/icfp25-ocaml5-js-docker), [post-POSIX IO](https://anil.recoil.org/notes/icfp25-post-posix) and [what I learnt](https://anil.recoil.org/notes/icfp25-what-i-learnt).
Synopsis: Highlights from ICFP/SPLASH 2025 including Hazel live programming, OCaml AI tooling, formally verified GC, and cross-community discussions between Haskell and OCaml.
Words: 2017
DOI: 10.59350/w1jvt-8qc58
## Related
- [.plan-26-08: At AI summit, Shriram's PL opinions, Zarr hacking](https://anil.recoil.org/notes/2026w8) (note, 2026-02-22)
- [.plan-26-07: Storage, Lego, Echo, and the IUCN](https://anil.recoil.org/notes/2026w7) (note, 2026-02-15)
- [The AI French Connection to the Practice of Science](https://anil.recoil.org/notes/entente-cordiale) (note, 2025-12-01)
- [Four Ps for Building Massive Collective Knowledge Systems](https://anil.recoil.org/notes/principles-for-collective-knowledge) (note, 2025-11-23)
- [A Roundup of ICFP/SPLASH 2025 happenings](https://anil.recoil.org/notes/icfp25) (note, 2025-10-10)
- [What I learnt at ICFP/SPLASH 2025 about OCaml, Hazel and FP](https://anil.recoil.org/notes/icfp25-what-i-learnt) (note, 2025-10-09)
- [It's time to go post-POSIX at ICFP/SPLASH 2025](https://anil.recoil.org/notes/icfp25-post-posix) (note, 2025-10-08)
- [Jane Street and Docker on moving to OCaml 5 at ICFP/SPLASH 2025](https://anil.recoil.org/notes/icfp25-ocaml5-js-docker) (note, 2025-10-07)
- [Holding an OxCaml tutorial at ICFP/SPLASH 2025](https://anil.recoil.org/notes/icfp25-oxcaml) (note, 2025-10-06)
- [Programming for the Planet at ICFP/SPLASH 2025](https://anil.recoil.org/notes/icfp25-propl) (note, 2025-10-05)
- [Three steps for OCaml to crest the AI humps](https://anil.recoil.org/papers/2025-ocaml-ai) (paper, 2025-10-01)
- [Webassembly on exotic architectures (a 2025 roundup)](https://anil.recoil.org/notes/wasm-on-exotic-targets) (note, 2025-04-16)
- [Bidirectional Hazel to OCaml programming](https://anil.recoil.org/ideas/hazel-to-ocaml-to-hazel) (idea, 2025-04-01)
- [Oh my Claude, we need agentic copilot sandboxing right now](https://anil.recoil.org/notes/claude-copilot-sandbox) (note, 2025-03-02)
- [Foundations of Computer Science](https://anil.recoil.org/notes/focs) (note, 2025-01-03)
- [Decomposable Type Highlighting for Bidirectional Type and Cast System](https://anil.recoil.org/papers/2025-decomposable-type-highlighting) (paper, 2025-01-01)
- [Gradually debugging type errors](https://anil.recoil.org/ideas/gradual-type-error-debugging) (idea, 2024-09-01)
- [Haskell Symposium 2014 Keynote on functional OS design](https://anil.recoil.org/videos/ed84b2eb-1b93-4dc3-b746-63a4af13d4ea) (video, 2014-09-05)
---
Canonical: https://anil.recoil.org/notes/icfp25-what-i-learnt
Type: note
License: CC BY 4.0
Tags: oxcaml, ocaml, programming, docker, multicore, functional, icfp
