TLDR Tech / InfoSec
Formal methods and the future of programming
Jane Street has reversed a 25-year stance against formal methods, having long judged the cost prohibitive (seL4 took 25 person-years to verify 8,700 lines of C, roughly 23 proof lines per code line). Agentic coding flipped that calculus: models lower the cost of constructing proofs while raising the payoff, since agent-generated code still trends toward slop that demands heavy review, and type-level universal guarantees kill entire bug classes like data races and XSS in ways tests cannot. The firm's deep control over OxCaml and a user base already primed for aggressive type-system features position it to bake proof-oriented techniques into the language itself, a bet that formal methods shift from niche assurance work to mainstream tooling as agents reshape where verification effort goes.
Read the full story