Formal methods and the future of programming
Points and comments are a snapshot, not live.
Jane Street shifts from skepticism to investment in formal methods, driven by AI-generated code verification needs.
Jane Street, historically skeptical of formal methods due to high costs (seL4 microkernel required 25 person-years to verify 8,700 lines), is now building a team to integrate formal methods into its OxCaml language. The shift stems from two changes: agentic coding lowers formal methods' cost by automating proof construction, and it increases their value by creating a verification bottleneck. AI-generated code tends toward "slop": overly complex, bug-filled, and inconsistent with codebase invariants. Formal methods provide universal guarantees (via type systems and proof techniques) that tests cannot achieve, and agents benefit from this structured feedback. Jane Street has advantages: deep language control and a programmer community eager for advanced type-system features. The company seeks formal methods experts for London and New York positions.
What commenters are saying
Commenters questioned whether sloppy AI-generated proofs solve the original problem. The leading counter-argument: formal proofs are self-verifying (they simply won't prove if wrong), reducing the verification surface to the specification rather than the entire codebase, though specifications themselves can balloon in complexity. One commenter noted that unlike most industries, Jane Street has the data, organizational maturity, and engineering sophistication to benefit from formal methods, but the approach may remain impractical for startups or less-structured domains. Another observed that AI automation of proof-writing parallels Rust's borrow checker, which users sometimes circumvent; defensive rigor at scale may be feasible only for established, well-modeled businesses.