Jane Street

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.

Caveat Configurator: How to replace configs with code, and why you might not want to

Jane Street engineers evolved from a naive dynamic plugin system plagued by versioning failures and tooling friction into a structured framework utilizing Config Generation and the centralized PlugD infrastructure to balance flexibility with safety. This transition replaced unmanageable runtime code execution with statically generated pure data files for standard cases, while reserving runtime plugins for scenarios requiring true dynamism under strict code review and library version management. By decoupling plugin distribution from application builds and enforcing mandatory testing, the firm successfully mitigates existential risks while allowing traders to safely deploy custom OCaml logic within production systems.

Heuristics and Biases

Sandor Lehoczky

Leveraging the foundational work of Daniel Kahneman and Amos Tversky, this presentation elucidates how human cognition relies on error-prone heuristics and the conflict between fast, intuitive System 1 thinking and slow, analytical System 2 reasoning. The discussion details empirical evidence of systemic biases such as loss aversion, anchoring, and confirmation bias, demonstrating their profound impact on diverse fields ranging from judicial parole decisions to financial market behavior. Rather than attempting to eliminate these innate flaws, the session advocates for strategic mitigation through meta-cognition, Bayesian updating, and the disciplined practice of overriding automatic responses to improve real-world decision-making outcomes.

Arjun Guha: On Verification for System Configurations Languages

Arjun Guha

Researchers developed "Rehearsal," a verification tool designed to detect determinism and idempotency violations in Puppet configuration manifests, which are frequent causes of major system outages. The system employs a transformation pipeline that converts complex Puppet syntax into Datalog and a low-level modeling language, leveraging the Z3 SMT solver alongside optimizations like partial order reduction and state pruning to analyze real-world code efficiently. Benchmarks on GitHub-scraped manifests demonstrate that this approach successfully identifies previously unknown non-deterministic bugs and generates fixes, although current limitations exclude shell script execution and specific file permission modeling.

How to Build an Exchange

Claudio, Ron, Pete

A US equities matching engine utilizes a deterministic, single-instance architecture to process three million messages per second while ensuring fair, latency-critical order execution across thousands of symbols. The system employs C++ and OCaml on a dedicated machine to replace complex distributed consensus with high-speed, single-threaded logic, allowing state machines to recover from failures within 30 to 60 seconds via message log replay. This design guarantees regulatory reproducibility and financial reliability by eliminating consensus overhead, enabling clients to achieve precise atomicity and global risk enforcement through simplified, high-throughput message sequencing.

Why Functional Programming Doesn't Matter

John Hughes, Tony Hoare

Jane Street, a high-frequency proprietary trading firm executing millions of daily trades, attributes its engineering success to OCaml's expressive static types rather than traditional functional features like laziness or strict purity. This type system enforces correctness by eliminating null pointer exceptions, forcing logic updates at compile-time to prevent bugs, and encoding business invariants to exclude impossible states. Consequently, the firm prioritizes predictable performance and verifiable clarity to protect its capital against errors, viewing advanced type systems as a more critical asset than higher-order functions or declarative purity.