A wide-ranging interview with Xavier Leroy, creator of OCaml, covering what sets OCaml apart from Rust and JavaScript, how type inference works (including the constraint-solving approach and how polymorphism emerges naturally), and a detailed explanation of formal verification — including proof assistants like Lean and Coq, the CompCert verified C compiler project, and the seL4 microkernel. The conversation also covers why multicore support took so long to add to OCaml (concurrent GC design and memory model challenges), how languages interface via FFIs, the dangers of near-correct LLM-generated code, and unsolved problems in programming language research.
296 Impressions