Formal methods and the future of programming

This post details the motivation and strategy for building a team focused on formal methods at Jane Street. It highlights how agentic coding changes the cost-benefit calculus of formal methods by reducing the cost of use and increasing the benefits through improved verification and agent feedback. The post also outlines Jane Street's unique advantages in this area, including deep control over their programming language (OxCaml) and a receptive community of programmers, and discusses potential near-term and long-term improvements and integration with external tools like Lean and Dafny.