Jane Street

Safe at Any Speed: Building a Performant, Safe, Maintainable Packet Processor

Sebastian Funk, JOSE ARRIETA

Jane Street engineers optimized their OCaml-based market data distribution system to handle NASDAQ's peak load of 4 million messages per second while maintaining zero-allocation on critical paths to avoid garbage collection delays. By leveraging PPX preprocessors, immediate integer options, and a domain-specific language for protocol generation, the team reduced per-message processing latency from five microseconds to under 750 nanoseconds. This approach demonstrates that strict single-core, low-latency performance targets can be achieved with high-level functional languages through aggressive inlining and careful memory management rather than resorting to lower-level systems code.

A Language-Oriented System Design

Nathan Linger

The Ontology system presents a dual-language architecture that manages organizational permissions through an English-facing interface backed by a dependently typed, deductive database engine. It distinguishes between hard-coded primitives, extensional tables, and intentional logical rules to enforce strict type safety, ensuring that data retrieval returns verifiable proof objects and automatically maintains referential integrity through cascading deletion and trash mechanisms. While the internal Prolog-like inference engine mitigates undecidability risks via execution budgets, the design allows for extensible permission modeling by uploading new type declarations without requiring code-level system upgrades.

Lindsey Kuper: Abstractions for Expressive, Efficient Parallel and Distributed Computing

Lindsey Kuper, Ron, Laura, Kunle Olokutun, Asante Toney, Neil Conway, Peter Alvaro, Carl, Nikki Vazou

The presentation outlines a unified framework for deterministic parallel computing that utilizes Lattice Variables (LVARs) and Conflict-Free Replicated Data Types to ensure correct distributed executions while enabling high-performance acceleration in Julia and Python through non-invasive domain-specific languages. Complementing these runtime systems, the speaker details a formal verification approach for safety-critical neural networks that employs lazy ReLU splitting within SMT solvers to manage the exponential complexity of non-linear activations. Future research aims to democratize solver development by integrating lattice theories directly into SMT architectures and verifying LVAR constraints through advanced type systems.

Jane and the Compiler

Jane, Yaron Minsky

Starting fifteen years ago as a tactical replacement for Python in quantitative research, Jane Street scaled its OCaml infrastructure to a 12-million-line production environment that now powers automated trading for its 800 employees. The firm drives significant ecosystem advancement by transitioning from passive user to active contributor, open-sourcing critical tools like the Dune build system while championing conservative language evolution and rigorous engineering features such as first-class modules and generalized algebraic data types. This strategic stewardship ensures the language remains performant and correct for high-stakes finance while securing long-term viability and attracting top engineering talent.

Marius Eriksen: Distributed, Incremental Dataflow Processing in the Cloud with Reflow

Marius Eriksen

The Braille bioinformatics team has developed Reflow, an open-source workflow engine designed to treat biological data pipelines as functional programs rather than static dependency graphs. By enforcing a strict data model and dynamic cloud resource provisioning, the system automatically parallelizes tasks, caches results through referential transparency, and ensures reproducible computations via versioned "data spaces." Currently adopted by Grail, the Chan Zuckerberg Institute, and several biotech startups, Reflow reduces infrastructure complexity while enabling efficient incremental updates to massive genomic and machine learning pipelines.

Introduction to Incr_dom: Writing Dynamic Web Apps in OCaml

Cristina Rosu

Jane Street engineers presented IncurDOM, an internal OCaml web UI framework designed to handle high-frequency updates and datasets exceeding 10,000 rows while avoiding browser lag. The demonstration highlighted how incremental computations, partial rendering, and strict adherence to the Elm architecture enable efficient state management and automatic code sharing between server and client logic. Attendees examined practical trade-offs against React and BuckleScript, noting specific optimizations like `IncrMap` that reduce reconstruction costs while identifying future needs for explicit component abstractions and dedicated testing tools.

OCaml All The Way Down

Andy Ray

This presentation outlines a hardware design framework utilizing the OCaml-based HardCAML domain-specific language to generate FPGA logic for custom peripherals like LED drivers, SPI sensors, and CORDIC math cores. The implementation targets the MicroBlaze soft CPU architecture, executing OCaml bytecode via a ZINC interpreter while leveraging standard Xilinx place-and-route tools to manage complex FPGA resources such as LUTs and DSP blocks. Future roadmaps prioritize full native CPU development within HardCAML, expanded formal verification using the Z3 solver, and the open-sourcing of testing infrastructure to reduce reliance on vendor-provided software components.

Effective Programming: Adding an Effect System to OCaml

This presentation details a comprehensive framework for algebraic effects that separates effect specification from implementation by treating operations like concurrency and state as explicit, resumable interruptions. It contrasts this approach with traditional monads to eliminate boilerplate and demonstrates a full conversion of the OCaml standard library, introducing syntax for tracking purity, region-based locality, and effect polymorphism directly in the type system. The work culminates in a runtime model where effect handlers manage heap-allocated call stacks while future extensions aim to enforce region safety and support multi-handler compositions for complex scenarios.

Types, and Why You Should Care

Ron

Hosted by the Recur Center at Jane Street, this third Localhost talk features speaker Ron, who argues that empirical data is insufficient for evaluating programming languages and that language choices must rely on intuition and specific trade-offs. Ron details how static type systems in languages like OCaml enhance performance, enforce critical invariants for security, and improve refactoring confidence compared to untyped alternatives, despite higher initial cognitive loads and verbosity. The discussion concludes by positioning types and testing as complementary mechanisms that reduce manual debugging, while highlighting the necessity of robust compiler tooling for adopting less mainstream languages.

Shriram Krishnamurthi: Curriculum Design as an Engineering Problem: Lessons from the Field

Shriram Krishnamurthi, Emmanuel Schanzer, Kathi Fisler, Laurie, Askle, James, Shetha, Eric Alata, Kathy, Dharan, Kenny, Yaron, Alice O'Neill, Papert

Bootstrap addresses critical equity and rigor gaps in computer science education by embedding computing concepts directly into mandatory Algebra, Data Science, and Physics curricula rather than relying on scarce specialized teachers or elective courses. This systems-engineering approach utilizes functional programming and a structured "Design Recipe" to scaffold mathematical thinking for all students, successfully mitigating the barriers of after-school programs and traditional silos. Facing scaling challenges due to limited administrative staff and bureaucratic resistance, the organization now prioritizes teacher professional development and is developing middle school modules like Bootstrap Junior to extend this integrated framework to earlier grades.

Bryan Cantrill: The Hurricane's Butterfly: Debugging Pathologically Performing Systems

Bryan Cantrill

Speaker argues that debugging pathological performance requires rejecting superstition and mechanical tuning in favor of rigorous observability to uncover root causes hidden within complex abstraction layers. By contrasting fatal crashes with elusive performance failures, the talk advocates for active instrumentation and visualization tools like state maps to distinguish symptoms from actual bottlenecks, as demonstrated in specific Sun E10K and Cassandra case studies. The presentation concludes that engineers must replace intuition with persistent data analysis to solve the "Software Paradox" where high-level bugs amplify into massive system-wide issues.

Echoes of Fourier

The event explains how complex numbers and the Discrete Fourier Transform decompose audio signals into frequency components to enable the $O(n \log n)$ Fast Fourier Transform algorithm. It further details how the Convolution Theorem applies these principles to efficiently model acoustic environments and audio effects like reverb through multiplication in the frequency domain. Finally, the presentation addresses the numerical challenges of reversing these processes via deconvolution for applications such as echo removal and digital room correction.

How Jane Street Does Code Review

Spiros

Jane Street engineers utilize Iron, a custom Mercurial-based review platform, to enforce mechanical code reading and branch-level state management that eliminates redundant reviews during rebases and merges. The system integrates feedback directly into source code and centralizes safety policies to support nested branch workflows, treating entire branch sequences as atomic units rather than individual commits. By combining a specialized Emacs client with a persistent task dashboard, the tool facilitates collaborative editing, automated file ownership obligations, and the review of non-code assets like configuration files and trading limits.

Nate Foster: Verifying Network Data Planes

Nate Foster, Bill Hallahan, JK Lee, Cole Schlesinger, Steffen Smolks, Robert Soule, Han Wang, Ron

Cornell Professor Nate Foster and Barefoot Networks have developed an automated verification tool for P4 programs running on programmable data planes to prevent catastrophic network failures caused by configuration errors. This system transforms P4 code into guarded commands to efficiently compute weakest preconditions using the Sacks and Flanagan algorithm, checking safety conditions against the Z3 SMT solver to generate counter-examples for invalid header accesses without requiring manual annotations. By modeling the separation between data and control planes through ghost state, the tool validates programs up to 20,000 lines of code in minutes, establishing a critical foundation for verifying complex software-defined network topologies.

Yudkowsky vs Hanson — Singularity Debate

Yudkowsky, Hanson

Eliezer Yudkowsky and Robin Hanson debated whether artificial superintelligence will emerge from a rapid, localized intelligence explosion or a gradual, decentralized accumulation across the global economy. While Yudkowsky argued that a small team could leverage hardware speed differentials to achieve a self-improving monopoly, Hanson countered that historical innovation patterns and the need for vast content would force AI development to remain integrated and shared. The post-debate audience vote shifted by seven voters to the "against" position, reflecting a narrow move toward Hanson's view that physical infrastructure and economic leakage prevent a single entity from instantly dominating the future.