GoKawiilI’ve been telling people for the last 25 years that Jane Street as an organization was just not interested in formal methods.
I’m not saying that anymore.
It’s not exactly that I think we were wrong all those years. To be clear, we’re strong believers in the power of tools to help us write better and more reliable code. And type systems are a kind of lightweight formal method that we’ve gotten an enormous amount of benefit from. So you might expect us to have been big believers in more full-on formal methods.
But outside of some special cases (notably, hardware synthesis), our sense has been that formal methods were just not worth the costs for us. And those costs are really high! seL4 is a great example of this. It’s a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.
Our hope is to make formal methods as pervasively useful of a tool for building software as sophisticated type systems are for us today.
That kind of approach could be worth it for a security-critical microkernel, where the stakes are high and the specifications are fairly clear. But it just doesn’t make sense for most software, and to us it didn’t feel like it made sense for even our most critical software.
But the emergence of agentic coding has changed our perspective, and we’ve gone from being skeptical to being excited about the possibilities. And as a result, we’re now building a team to focus on formal methods. Our hope is to make formal methods as pervasively useful of a tool for building software as sophisticated type systems are for us today.
Why the change of heart?
Agentic coding upsets the formal-methods apple-cart in a few ways.
For one thing, it dramatically changes the cost of using formal methods. It’s not that agents can on their own construct arbitrarily challenging proofs. But models are enormously helpful, and broaden the set of people who can use these tools productively. With formal methods being easier to use than ever, it’s worth reconsidering the old cost/benefit calculus.
... continue reading