If the spec is complex you are probably proving the bugs in the spec are indeed correctly implemented...

Edit: that said, spending the formal spec time will probably reduce the number of bugs far below than what we find normal now. But money...

Yeah and then the specification at that level of specificity IS the code. How do you prove the specification is bug free?

Define what is a bug in a spec? I defined the program to do one thing and one thing only. What does does it mean when I have a bug in my definition? There's a definition for the definition? Makes no sense.

You can argue that no code ever has bugs by that logic, after all you defined the program to do one thing, and it did it, it was merely human expectation that was in error.

That's what I'm arguing. Code can be proven correct against a formal spec.

However, because we don't do proofs in software, there are bugs.

Code is itself a specification.

It can be, but generally it is not.

It means that the one thing you defined it to do was not the right thing.

> Bugs can arise where programs intersect in the real world.

Well, the context is flight control software for airplanes. If that code is bug-free but doesn't intersect the real world, that's rather useless. And if it intersects the real world but therefore is not bug-free, that's not a great argument for proofs of formal correctness.

But all of that is kind of beside the point. The MCAS specification was the wrong thing. Proving the implementation correct is useless. (You asked what is a bug in a spec? MCAS shows you the answer. Only taking input from one sensor is the wrong thing. Repeatedly applying nose-down is the wrong thing. It seems like I'm missing one or two more.)

You can prove the code correct against the spec. However you can't prove that the spec will do what you expect it to do because the spec is where the intersection with the real world occurs. Therefore, you must test the spec. Everything that falls under the spec can be formally verified to 100% correctness.