The OCaml Planet RSS

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

This talk breaks down a CTF puzzle Corwin de Zahr designed a few years back that involves finding problems and vulnerabilities within the OCaml runtime. Read the full transcript here: https://www.janestreet.com/tech-talks/hacking-ocaml/

This talk breaks down a CTF puzzle Corwin de Zahr designed a few years back that involves finding problems and vulnerabilities within the OCaml runtime. Read the full transcript here: https://www.janestreet.com/tech-talks/hacking-ocaml/

Rust promises to empower everyone to build reliable software, but its unique features create steep learning curves. In this talk, Will Crichton presents four years of research into evidence-based tools that help both novices and experts work more effectively with Rust's complexity, including: - Ownership visualization: Interactive diagrams showing permissions (read/write/own) that help students understand borrowing better than rule-based explanations - Trait debugging: A graphical tool for navigating complex trait inference trees when compiler errors become unreadably long - Program slicing: Using Rust's type system to automatically highlight only code relevant to specific variables All tools discussed are open source and available for use.

Jane Street is an electronic trading firm that uses low latency trading systems built in OCaml to provide liquidity to financial markets worldwide. In December 2022, after nearly a decade of development, OCaml 5.0 was released with OCaml’s first multi-core capable runtime. This was an exciting milestone, finally making it possible to write shared-memory parallel programs in OCaml. The new runtime was designed to be easy to adopt: it didn’t disturb OCaml’s FFI, and performance was meant to be only a few percentage points slower in single-core mode. Despite those promising beginnings, switching to runtime-5 within Jane Street was harder than we expected. Indeed, we've only just switched to it this year, after 2.5 years of research and engineering effort. This talk will give an overview of the problems we ran into, and what we learned from the process, including some new ideas that solved some very old problems in the design of OCaml's GC. Read the full transcript here: https://www.janestreet.com/tech-talks/the-saga-of-multicore-ocaml/

Jane Street is a trading firm that uses a variety of high-performance systems built in OCaml to provide liquidity to financial markets worldwide. Over the last couple of years, we have started developing major extensions to OCaml’s type system, with the primary goal of making OCaml a better language for writing high-performance systems. In this talk, we will attempt to provide a developer's-eye view of these changes. We’ll cover two major directions of innovation: first, the addition of modal types to OCaml, which opens up a variety of ambitious features, like memory-safe stack-allocation; type-level tracking of effects, and data-race freedom guarantees for multicore code. The second is the addition of a kind system to OCaml, which provides more control over the representation of memory, in particular allowing for structured data to be represented in a cache-and-prefetch-friendly tabular form. Together, these features pull together some of the most important features for writing high performance code in Rust, while maintaining the relative simplicity of programming in OCaml. In all of this, we will focus less on the type theory, and more on how these features are surfaced to users, the practical problems that they help us solve, and the place in the design space of programming languages that this leaves us in. Read the full transcript here: https://www.janestreet.com/tech-talks/making-ocaml-safe-for-performance-engineering/

Over the last 10 years we've seen Machine Learning consume everything, from the tech industry to the Nobel Prize, and yes, even the ML acronym. This rise in ML has also come along with an unprecedented buildout of infra, with Llama 3 now reaching 4e25 floating point operations, or 40 yottaflops, or 40 trillion trillion floating point operations. To build these ML models, you need ML systems, like PyTorch. In this talk, Horace will (attempt to) answer: - How have ML systems evolved over time to meet the training needs of ML models? How does building ML systems differ from regular systems? - How do we get the most out of a single GPU? What's the point of compilers if we're just training a single model? - And what is the right way to think about scaling to 10s of thousands of GPUs?

In this Tech Talk, Tudor Brindus, a software engineer at Jane Street, shares his expertise on reducing jitter—deviations from mean input processing times—in low-latency systems. Maintaining consistently low jitter in a trading system allows us to offer tighter markets without incurring additional risk. Using a simple memory ping-pong application as a case study, Tudor will walk through how to identify and resolve common sources of jitter caused by both Linux kernel and microarchitectural conditions.

Charlie Marsh is the founder of Astral, which develops uv, a next-generation Python package manager written in Rust. In this talk, Charlie details the unique challenges of the Python packaging ecosystem and how he made uv so fast: allocators, concurrency, zero-copy tricks, and more. You can find the transcript for this video and other Tech Talks here: https://www.janestreet.com/tech-talks/index.html

Presented by: Raph Levien The GPU in a modern computer (desktop or mobile) has about an order of magnitude more raw general purpose computing throughput than the CPU, but is barely used except for games, machine learning, and cryptocurrency mining, largely because it’s hard to program. Getting good performance entails massive parallelism (thousands of threads) and careful attention to an explicit memory hierarchy. While GPU compute programming may seem to many like a black art, techniques from functional programming, including immutable data structures and an emphasis on associative operations (monoids) adapt very well to this space. This talk will present techniques used in piet-metal, a new 2D graphics rendering engine optimized for the modern GPU compute, and hopefully will serve as an invitation for the curious to explore this strange but powerful computing environment. Raph Levien is currently an independent researcher exploring 2D graphics, font technology, and GUI, doing most of his work in Rust. Previously he was at Google for 11 years, including on the Android UI toolkit team, mostly working on fonts and text, and before that was the maintainer of Ghostscript. He has a PhD in Computer Science from UC Berkeley, on the topic of curve design tools.