I understand what you mean but no tester/developer worth their salt should say or hide behind this. Sadly, too many do. The job of the tester is to go beyond just blindly testing the spec but to find and report faults, those that somehow were missed earlier in the chain. And oh, no idea how Boeing missed it but some Indian companies are just not worth the bother. HCL, TCS, Cognizant, Infosys included. But hey, they're cheap!

> The job of the tester is to go beyond just blindly testing the spec but to find and report faults, those that somehow were missed earlier in the chain.

So these testers should have been test pilots? - because the interaction of MCAS and the difficulty in manual trimming was not going to be found until someone tried it in the air (there is considerable doubt as to whether simulators accurately model it.)

And if this was the tester's job, what was the job of the engineers at Boeing who decided on using MCAS to solve a problem, and those at the FAA who endorsed it?

You obviously missed my point, so kindly re-read my comment, particularly the part about the entire chain. Everyone involved is responsible for the deaths of innocent lives. Testers are at the end of the chain and have the power of approving or halting the deployment but the ones working for these inferior companies don't put on their thinking caps because they're just incapable of doing so. They test the spec and collect the check.

I read and understood your original point, and that is what I disagree with. You have made a general point about responsibility, but my point is that if we look at the specifics of this particular issue, one cannot expect software testers to anticipate the particular risks that MCAS presented. On the other hand, there are other roles in the airplane development process where the people involved are expected to have the requisite knowledge to identify and judge such risks, and these are employees of Boeing or the FAA (if it turns out that these roles were farmed out to low-bidding subcontractors, that's a separate issue.) These domain experts ruled that MCAS was acceptable as designed, apparently largely on the mistaken grounds that MCAS failure is just like any other trim runaway excursion, a mistake exacerbated by the failure to properly communicate the increased power of the redesigned MCAS among the domain experts.

No sound root-cause analysis will come to the conclusion that the crashes resulted from Boeing contracting out software testing to low-bid contractors. You are making the fallacy of arguing a general point that does not apply in this specific case.

That's why you want devs who actually care about the business. Often a tough sell for management who do not expect feedback/collaboration from development; and that's also a skill that devs actually have to practice to get good at, else if you just ask them they give self-interested answers (cutting features etc..)

If so, this may be a good back-to-reality counter-example for all the over-zealous formal proof enthusiasts. There is an old paper from 70's by people who designed complex systems where they stress the point that even if your system was designed and formally checked and if it obeys all the known rules and specifications, it will still fail in real world unless you test and iterate it a lot. Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. One has to experiment/iterate to find the very specifications that are then going to be designed against. Which in 737Max case was seemingly neglected.

> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real.

You cannot exhaustively test software either - the number of cases to cover are beyond astronomical.

The effectiveness of both specification and testing ultimately depend on the same thing: thinking of all the relevant possibilities. If you overlook a possible failure mode, there's no guarantee it will be caught at any phase. The main benefit of formal methods, I think, is that the rigor tends to make such oversights visible.

the only people who think formal methods are a magic bullet are those who have not tried them. Likewise, the only people who think more testing (and especially unit testing) is a magic bullet are those who don't understand combinatorial complexity.

> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real.

Is that so? Wouldn't it be in theory possible to verify it against our current understanding of all laws of physics and the corresponding equations?

You are forgetting nondeterministic aspects. Only in theory, aircraft and atmosphere is a deterministic Newtonian machine, in practice, less so. But even if so, physics simulations can't be done and evaluated for all possible initial conditions for even the simplest model.

One can imagine a mental model of airplane and make a formal design for it. Then do a formal check in the most important scenarios that introduce weather, human action, system failures. The design will always fail for some scenarios. Not a problem if those are not important (in terms of risk). But which scenarios are the important ones? Probability and severity of consequences of those scenarios are much needed knowledge, and one can find those only via the good old method of iterative testing in wild.

But it obeys the laws of physics perfectly as it nosedives into the ground.

It also has a user interface. Are you saying it's possible to formally quantify human behaviour as well?

Every program has a inputs, and with that some more ore less direct version of a user interface. You define the acceptable input values and then define what happens with unacceptable ones (and same for combinations).

If that were not verifiable, then no program would be.

Anyone that has ever worked with outsourced developers knows the truth of this.

If you give them a spec or requirements, they will do exactly what that thing says. Even including the typos or grammatical errors.

I don’t blame them. They have no incentive to care beyond this type of business transaction.

But applying this model to anything other than vaporware is terrifying.

> They have no incentive to care beyond this type of business transaction.

I don't know if it's even a matter of incentive. Even when we hire local developers from some particular cultures, it's not part of their culture to question "authority" or be independent thinkers. So, they too will do exactly what we ask because they trust us as the experts or think that we'll be displeased if they don't do precisely what we asked.

Sometimes including the typos is important!

https://en.wikipedia.org/wiki/HTTP_referer

About typos, if the typo is part of the spec, that's what the software should implement. If the spec gets revised, then the programmers should implement the revised version.

When you have software that interacts with other software, you follow the spec because you know the spec is going to be followed by the other parts, and that you should not get imaginative when human lives depend on your software working correctly.

The MCAS incident shows software that worked as expected, based on a spec that had incorrect and missing information and pilots that didn't have the information to understand the erroneous behavior. Also, the motors that actuate the trim wheels exert so much force that the pilots weren't able to counteract their action.