Formal Methods and the Future of Programming

5 hours ago

Jane Street previously viewed formal methods as too costly for most software, with exceptions like hardware synthesis, despite valuing type systems as lightweight formal methods.
The rise of agentic coding has shifted their perspective, making formal methods more feasible due to reduced costs and increased benefits in verification and feedback for AI-generated code.
They are now building a team to integrate formal methods more deeply, leveraging their control over the programming language (OxCaml) and an engaged user base to explore both near-term and long-term improvements.
Formal methods are seen as a solution to the verification bottleneck with AI code, providing universal guarantees that tests alone cannot, and enhancing agent training through structured feedback.
Jane Street's environment offers unique advantages for this work, including community support for advanced language features and the ability to innovate internally while drawing inspiration from external PL tools.

Hasty Briefsbeta