Jane Street on formal methods and the future of programming

Category: Engineering post
Status: discussion
Sources: Jane Street blog, HN discussion
Summary: In a post dated 2026-06-07, Yaron Minsky writes that Jane Street, after 25 years of treating formal methods as not worth the cost outside special cases like hardware synthesis, is changing its position. The post frames type systems as a lightweight formal method the firm already relies on heavily, uses the formally verified seL4 microkernel as a reference point for the historical cost of full verification, and argues that the economics are shifting. It surfaced as the top post on both Hacker News (228 points) and r/programming.
Why it matters: A large OCaml-centric trading firm reconsidering formal methods is a signal that verification tooling is moving closer to the cost threshold for mainstream production engineering.