The OCaml Planet RSS

Ortac 0.8.0 generates QCheck-STM test suites that check OCaml libraries for parallel safety with multiple SUTs. Here are the design choices behind it.

This year, for the first time, the Functional Programming Workshops were held in Paris, on Inria's, the French National Computer Science Research Institute, campus along with a watch party for the ICFP conference at Indianapolis. As each year we attended the OCaml Workshop to see the latest advances...

day10 now runs side-by-side with OBuilder on the RISC-V opam-repo-ci workers, and the layer cache shows why it wins. Plus the Lwt bug that stopped Windows workers reconnecting to the scheduler, an LTSC 2022 image that hadn’t built in months, and ocaml.org taken down by a 371 MB search index.

Mathematics gets its AI reckoning after security, thinking through formative assessment for the CST Tripos, triaging Scrutineer bugs without panicking, and an Echo Labs visit.

Rooted in Cyrus Omar's group's work on the Hazel live programming environment, this talk presents a vision for a "live type-theoretic computational commons": a shared monorepo where humans and swarms of AI agents make verifiable progress on parallel coding tasks. The collaboration model combines novel editing primitives (e.g. CRDT-based structure editing and Unison-style versioning) with familiar type-theoretic structure (e.g. OCaml-style modules and interfaces, Isabelle-style proofs). Two research problems take center stage. First, large-scale collaboration requires that incomplete programs remain continuously analyzable and executable — Cyrus will present recent foundational work on live, incremental type checking and evaluation of programs with typed holes. Second, as agent swarms grow in size and ambition, giving them direct terminal access to our machines and data becomes more risky. He will present a type-theoretic object-capability architecture that provably bounds agent behavior, with per-task capability signatures shaped by humans and weak AI supervisors to enforce the principle of least authority. 00:00:00 – Feedback loops, from pianos to compilers 00:03:29 – The gap problem in dev tools 00:05:07 – A live demo of Hazel: writing quicksort 00:06:19 – Holes, error recovery, and live probes 00:10:14 – "Oops, all threes": debugging with real data 00:12:42 – Demo questions: purity, holes, and call frames 00:25:56 – Graphical notation: tables, dials, and music 00:29:26 – Agentic harnesses and swarms of agents 00:33:33 – Incrementality: re-execution and type checking 00:36:56 – Live incremental IDEs for AI agents 00:41:19 – Collaborative editing for thousands of agents: Grove and Unison 00:44:32 – "Dangerously skip permissions" and object capabilities 00:47:02 – A live computational commons, from Wikipedia to climate models 00:50:24 – Audience Q&A

A refreshed set of Part II and MPhil projects, split between environmental science problems that need computer science, and more conventional systems and programming languages topics.