[lmm]

> QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each.

And formal proofs don't make your confidence higher? IME they're the most efficient tool in the toolbox if you need to get to really low defect rates. (Of course, the sad economic reality is that for most consumer software even a 5% defect rate is perfectly acceptable).

[zzzcpan]

It's not that simple. Defects don't necessarily have to cause problems, depending on how you design your software (think OTP-style architecture). And avoiding problems is in fact what you always need, not low defect rates. It's just so happens that sometimes you can only achieve decent reliability by pursuing very low defect rates. But for a lot of software it cannot economically beat other approaches.

[abritinthebay]

Given a formal proof of a complex system that doesn’t contain any assumptions or mis-modeling is - practically speaking - unachievable...

... then in comparison the time is better spent on something that will produce demonstratable results, even if imperfectly applied.

And that is QA & testing.

[lmm]

> the time is better spent on something that will produce demonstratable results, even if imperfectly applied.

How is formal proof not such a thing?