Latest Interviews

Production Engineering When Trading Billions of Dollars a Day

Mark Doss

Mark, a production engineer at Jane Street, outlines a high-stakes trading environment where even a 0.01% error rate can trigger insolvency, necessitating a monitoring strategy that rejects standard service level objectives in favor of code-level, event-based alerts. The firm employs a defense-in-depth approach using redundant, symptom-focused detection systems to catch catastrophic failures like fat-finger trades or stale market data before they cascade. By integrating deep domain knowledge into incident response and treating monitoring infrastructure as more critical than the trading systems themselves, Jane Street ensures that traders and engineers collaborate to resolve unique operational risks with extreme precision.

The Cost of Concurrency Coordination with Jon Gjengset

Jon Gjengset, John, Gabriel Kreiman

The presentation challenges the conventional view that mutexes are inherently slow, demonstrating instead that performance degradation in high-concurrency environments stems from CPU cache coherence overheads and MESI protocol costs rather than the lock mechanism itself. To address false sharing and serialization issues found in reader-writer locks, the speaker details the Left-Right data structure, a lock-free architecture that achieves linear scaling for read-heavy workloads by decoupling reader access from writer synchronization. Finally, the discussion emphasizes that optimal synchronization strategy depends on the specific read-to-write ratio and consistency requirements, urging developers to profile cache behavior and avoid blind optimization of lock primitives.

Matt Godbolt: Advanced Skylake Deep Dive

Matt Godbolt, Jesper

Matt Godbolt, a prominent C++ developer transitioning to HRT, presents a detailed reverse-engineered analysis of the Skylake-era CPU microarchitecture based on community findings rather than official documentation. The talk dissects critical pipeline stages including the front-end's instruction decoding, the micro-op cache limitations, and the complex register renaming mechanics that define the processor's performance characteristics. Key revelations include specific hardware flaws like the Loop Stream Detector bug, port allocation strategies, and the diminishing returns of increasing architectural register counts compared to the hundreds of physical registers already available.

Arjun Guha: How Language Models Model Programming Languages & How Programmers Model Language Models

Arjun Guha

Arjun Guha presents a comprehensive analysis of large language models in programming, highlighting how traditional benchmarks are saturating while new methods like multi-PLE and language-agnostic transforms reveal significant performance gaps in low-resource languages such as OCaml. Through mechanistic interpretability techniques like activation steering, the talk demonstrates that internal model vectors can effectively correct type prediction errors and switch target languages without retraining, exposing shared representations across diverse syntaxes. These technical insights are contextualized by human studies showing that student success in prompting models hinges on providing specific semantic clues rather than syntactic fixes, while industry data reveals a surge in AI co-authorship alongside complex debates regarding actual productivity gains.

Neil Mitchell: Pyrefly: Type Checking 1.8 Million Lines of Python Per Second

Neil Mitchell, Roman

Meta engineer Neil Mitchell introduced PyreFly, an open-source Python type checker reimplemented in Rust to address performance and scalability limitations for massive codebases like Instagram. The tool utilizes an aggressive memory eviction strategy and file-level concurrency to deliver rapid IDE feedback while supporting complex type features such as structural subtyping and flow narrowing. Released under the MIT license with over 100 contributors, PyreFly aims to replace legacy systems by prioritizing broad ecosystem adoption and seamless integration with build tools like Buck.

Will Crichton: Rust for Everyone!

Will Crichton

Will Creighton's research at the Cognitive Engineering Lab applies human-centered design and formal cognitive theories to address fundamental learning and debugging barriers in Rust. By developing three core tools—Aquascope for visualizing ownership permissions, Argus for interactive trait solver trees, and Flow History for precise program slicing—the team achieved a 9-point score increase in learner assessments and a threefold speedup in error localization during user studies. Future efforts are now directed toward resolving async/await complexities and promoting extensible IDE frameworks like CodeMirror to further advance a scientific approach to programming language design.

Making OCaml Safe for Performance Engineering

Mark

Jane Street's research introduces a suite of OCaml extensions featuring unboxed types and stack allocation to eliminate memory waste and garbage collection overhead in performance-critical applications. These innovations expand into a static mode system that guarantees data race freedom for parallel execution by enforcing lifetime and portability constraints without explicit annotations. Currently deployed in production for memory management features and undergoing beta testing for concurrency safety, this work aims to integrate into mainline OCaml while earning a POPL award for its formal verification of race freedom.

Horace He: Building Machine Learning Systems for a Trillion Trillion Floating Point Operations

Horace He

Meta compiler engineer Horace He analyzes the dramatic consolidation of AI infrastructure, noting that modern model training now requires massive power resources and billions in capital to achieve state-of-the-art performance. He details how the industry has transitioned from simple imperative execution to complex compiler strategies like FlexAttention and `torch.compile`, which are essential for managing the critical balance between GPU compute and memory movement. Ultimately, He argues that the primary challenge in this field is shifting focus from pure optimization to designing robust programming models that allow developers to reliably express complex performance trade-offs in large-scale distributed systems.

Matt Might: The Algorithm for Precision Medicine

Matt Might, Matt Mite

Matt Mite, director of the Hugh Call Precision Medicine Institute at UAB, leverages computational optimization and a knowledge graph of 30 million abstracts to derive actionable precision medicine strategies for patients with undiagnosed genetic disorders. His approach, exemplified by the successful treatment of his son Bertrand's NGLY1 deficiency and the identification of Prevacid for ion channel epilepsies, prioritizes logical mechanism proofs to overcome physician skepticism and legal liability. Through an undergraduate-led workflow and the "All of Us" initiative, Mite's institute continues to transform complex genomic data into targeted interventions, from drug repurposing to novel metabolic pathways, asserting that scientific experimentation always yields actionable solutions.

Derek Dreyer: RustBelt: Logical Foundations for the Future of Safe Systems Programming

Derek Dreyer, Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Hoang-Hai Dang, Jan-Oliver Kaiser

The MPI for Software Systems' "Rust Belt" project applies decades of academic research to formally verify the safety guarantees of the Rust programming language against the risks posed by "unsafe" code. By leveraging the Iris framework and mechanizing proofs in the Coq assistant, the team establishes a semantic safety model that independently verifies complex libraries like `Arc` and `Mutex`, successfully identifying critical bugs in memory ordering and reference counting. This methodology ensures that future language evolution and standard library modifications can proceed with mathematical certainty that undefined behavior remains impossible.

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.

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.

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.

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.

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.