Latest Interviews

Real Numbers – Episode 15, The Half Court Shot

Sawyer

Host discusses probability theory by solving a problem where a student named Jayden schedules two or three exams across five weekdays, calculating expected spans of 1.6 and 2.4 days respectively through enumeration and linearity of expectation. The episode transitions to a new challenge involving a basketball player named Danielle who makes 20% of her half-court shots, asking listeners to determine the expected attempts needed for a single success and for two consecutive makes. While the mathematical framework for the exam scenarios is fully derived and verified, the solution to Danielle's geometric distribution problem remains pending for the listener to solve.

Real Numbers – Episode 13, How Many Snowboards Need Sharpening

Sawyer

This instructional session applies the linearity of expectation to calculate expected values in scenarios involving both independent and dependent selections. Using the marching band example, the analysis demonstrates how fixed global distributions alter probabilities while the method for summing indicator variables remains valid regardless of independence. The presentation concludes by challenging the audience to utilize this specific probabilistic framework to determine the expected number of snowboards requiring sharpening in a student-led lesson environment.

Real Numbers – Episode 12, Photographing the Chaotic Marching Band

Sawyer

The episode explores expected value and the linearity of expectation by first applying these concepts to a conditional probability problem involving a haunted forest monster. The instructors update monster type probabilities based on a 4-damage roll to calculate a resulting expected value of 5.5 for the second attack. The session concludes by introducing a problem of the week that contrasts independent choice scenarios with fixed pool distributions to determine the expected number of synchronized rows in a marching band.

Real Numbers – Episode 11, The Unknown Monster

Sawyer

The episode calculates the expected damage of a random monster attack by weighting uniform distributions across three difficulty tiers and determines the conditional expectation of a second attack following a four-damage outcome. A prior review solves the geometric optimization of a painting passing through a composite window, utilizing the Power of a Point theorem to prove the maximum height corresponds to the Golden Ratio. Both segments demonstrate how probabilistic weighting and geometric theorems can simplify complex mathematical problems into elegant, closed-form solutions.

Real Numbers – Episode 08, Crossing the River

Sawyer

Host Sawyer presents a physics challenge where viewers must calculate the precise aiming angle required for a boat traveling at an unknown speed to cross a 100-meter wide river with an unknown current and land at a specific downstream dock. The segment also revisits a previous geometry problem, confirming that reshaping a hemispherical slush cone involves removing a 3-cm radius circular section and moving a volume of $40\pi/3$ cubic centimeters. Sawyer concludes the episode by inviting the audience to submit their navigational bearings and diagrams for the river crossing solution.

Real Numbers – Episode 05, Grandma's Secret College Fund

Sawyer

This episode concludes a probability series by applying Bayes' theorem to a piggy bank scenario where a drawn $20 bill updates the prior probability that a grandmother added either a one or twenty-dollar note on Sunday. The discussion briefly recapitulates a previous DMV exam study analysis that established a 73.3% probability of an applicant having studied given they passed. To finalize the segment, the hosts invite viewers to submit their solutions to the piggy bank problem and propose mathematical topics for the upcoming transition to geometric problems.

Real Numbers – Episode 03, A Perfectly Balanced War

Sawyer

In a "Real Numbers" segment, hosts analyze probability within the card game War using a reduced 26-card deck where Clara holds all Clubs and Damien holds all Diamonds to calculate the likelihood of Clara winning an Ace in the first battle. The episode explains how to solve this dependent event problem using conditional probability formulas and contrasts them with previous methods for finding consecutive taxi sequences, specifically the state machine and inside-out logic approaches. Viewers are encouraged to submit their own calculations for the card game scenario and propose mathematical extensions for future episodes.

Real Numbers – Episode 01, The Perils of Dogsitting

Sawyer

Host Sawyer presents a weekly mathematical analysis program where viewers submit solutions to real-world probability problems, beginning with a scenario involving a dog named Fluffy that wakes its sitter with a two-thirds probability on any given night. The episode establishes fundamental probability rules, including the calculations for independent, disjoint, and non-disjoint events, to guide participants toward determining the likelihood of at least two full nights of sleep within a five-day period. Sawyer confirms that the solution to the specific dog-sitting challenge and a subsequent new problem will be explored in the following broadcast.

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.