[agentultra]

Given a formal model or proof of a system and the two teams will either succeed or fail.

Give them a specification in prose and they will have a little too much wiggle room. Such specifications are useful to a degree but I look at them like sketches on a napkin.

If you use a more formal method of mathematics as your specification then you can be more precise about the invariants that matter and model your system more faithfully. And with a good proof assistant or model checker the computer can even help you catch flaws in your design that you would never have been able to think of on your own.

It's true that the source code is a proof of something. It often helps to know whether you've built the right thing. And that it does what you think it does.

[wvenable]

Given a sufficient model or proof of the system and you don't need the teams at all -- they can be automated away.

Getting your model right is as hard, if not harder, than getting the software right in the first place. The problem hasn't changed you've just added more layers (and more cost) in the hopes that doing it twice, differently, eliminates most of the problems.

[agentultra]

For some trivial small problems writing a model in TLA+ or Lean is definitely more costly than just writing the software even if you get a few things wrong. It'd be like commissioning a blueprint for your shed in the backyard. For those sorts of tasks it is sufficient to just write a few tests and call it a day.

However for more complex services that are trying to manage several clusters of resources amongst tens of thousands of tenants or more there are invariably going to be errors. The kinds of errors you see might require a particular series of events to change your state in 53 steps to hit it... but if you're servicing > 1M requests in a minute that ends up being frequent enough to be bothersome.

Even more so if you're working on a memory controller in a new hardware platform that is expected to ship in a few million units. It'd be nice to know that you have strong evidence that your system is correct.

And developing models is hard but so is thinking. Nobody said it was easy. But one shouldn't say that we can't engineer robust software systems. It's just patently false.