[wvenable]

Specifications and design documents are merely estimations. If you've made every single decision possible, you've written the software.

If you have blueprints for a bridge and get two different companies to build it, you'll get the same bridge both times. The differences, if any, would be minor.

If you give specifications and design documents to two software teams you could get radically different products that look nothing alike and it's entirely possible that neither one of them will satisfy the clients needs.

[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.

[Jtsummers]

If they don't meet the clients needs then they were the wrong spec and design document.

Honest question: without a specification, how do you verify your software?

[wvenable]

There is plenty of software that is driven entirely by specification. Inputs come in and outputs go out. And you validate that with a test suite, etc.

But even more software is designed not for machine-machine communication but for machine-human interaction. And humans are notoriously bad at knowing what they want and need. In some cases, the existence of software so fundamentally changes the nature of work that humans don't even have the frame of reference necessary to provide full specifications. Yet the software still has to be written, do it's job, and be accepted. I'm not sure I have an answer to your question but somehow I still get the job done.