How the Boeing 737 Max disaster looks to a software Developer • Hacker News Board

Re: How the Boeing 737 Max disaster looks to a software Developer

#31

Post by teddyh » Thu, Apr 18, 2019, 9:16 PM UTC

crimsonalucard wrote: post #2

The irony of software is that it is the only discipline in engineering where results can be proven with logic. Yet we still do testing on it as if it was a blackbox.

I refer you to Joel Spolsky about formal proofs of programs:

[…]

So in the first day of that class, Dr. Zuck filled up two entire whiteboards and quite a lot of the wall next to the whiteboards proving that if you have a light switch, and the light was off, and you flip the switch, the light will then be on.

The proof was insanely complicated, and very error-prone. It was harder to prove that the proof was correct than to convince yourself of the fact that switching a light switch turns on the light. Indeed the multiple whiteboards of proof included many skipped steps, skipped because they were too tedious to go into formally. Many steps were reached using the long-cherished method of Proof by Induction, others by Proof by Reductio ad Absurdum, and still others using Proof by Graduate Student.

For our homework, we had to prove the converse: if the light was off, and it’s on now, prove that you flipped it.

I tried, I really did.

I spent hours in the library trying.

After a couple of hours I found a mistake in Dr. Zuck’s original proof which I was trying to emulate. Probably I copied it down wrong, but it made me realize something: if it takes three hours of filling up blackboards to prove something trivial, allowing hundreds of opportunities for mistakes to slip in, this mechanism would never be able to prove things that are interesting.

https://www.joelonsoftware.com/2005/01/02/advice-for-compute...

Re: How the Boeing 737 Max disaster looks to a software Developer

#32

Post by laydn » Thu, Apr 18, 2019, 9:19 PM UTC

The article states: "When MCAS senses that the angle of attack is too high, it commands the aircraft’s trim system to lower the nose. It also does something else: It pushes the pilot’s control columns downward"

No, it does not push the pilot's control columns downward.

Re: How the Boeing 737 Max disaster looks to a software Developer

#33

Post by tluyben2 » Thu, Apr 18, 2019, 9:19 PM UTC

mikeash wrote: post #30

tluyben2 wrote: post #15

Earlier quoted context omitted.

It would ensure people thought about it a lot longer and harder than without those proofs, so the code had a whole lot more critical thinking done over it. Seems worth it in some areas like airplanes.

The trouble with formal proofs is that you can only prove that the code does what you say it does, not that it does what it needs to do. MCAS performed as designed. Only reading one AoA sensor, acting on bad readings, not rejecting values that are clearly out of bounds, operating continuously without any limits on its pitch authority, all of this was how is was designed to work. You could have proved MCAS “correct” a…

Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.

Re: How the Boeing 737 Max disaster looks to a software Developer

#34

Post by paulopontesm » Thu, Apr 18, 2019, 9:19 PM UTC

murkle wrote: post #19

> In the 737 Max, only one of the flight management computers is active at a time—either the pilot’s computer or the copilot’s computer. And the active computer takes inputs only from the sensors on its own side of the aircraft.

Also wondered what was the logic behind this decision...

Re: How the Boeing 737 Max disaster looks to a software Developer

#35

Post by threatofrain » Thu, Apr 18, 2019, 9:21 PM UTC

crimsonalucard wrote: post #2

The irony of software is that it is the only discipline in engineering where results can be proven with logic. Yet we still do testing on it as if it was a blackbox.

Mathematicians often don't rely on the exact correctness of a proof's description, instead relying on a rough sketch of strategy.

Re: How the Boeing 737 Max disaster looks to a software Developer

#36

Post by _bxg1 » Thu, Apr 18, 2019, 9:21 PM UTC

"Various hacks (as we would call them in the software industry) were developed."

Dear God. That's a sentence I never, ever wanted to hear about an aircraft.

Re: How the Boeing 737 Max disaster looks to a software Developer

#37

Post by mikeash » Thu, Apr 18, 2019, 9:22 PM UTC

tluyben2 wrote: post #33

mikeash wrote: post #30

Earlier quoted context omitted.

The trouble with formal proofs is that you can only prove that the code does what you say it does, not that it does what it needs to do. MCAS performed as designed. Only reading one AoA sensor, acting on bad readings, not rejecting values that are clearly out of bounds, operating continuously without any limits on its pitch authority, all of this was how is was designed to work. You could have proved MCAS “correct” a…

Yes, agreed, but for life or death situations, as a programmer, I would prefer to use all tools at our disposal; besides money it does probably improve the quality if you spend this time.

I think this is likely to be true, but I do wonder if there might be a better way to spend those resources. For this particular example, you’d have been better off putting more money into flight testing with various sensor errors.

Re: How the Boeing 737 Max disaster looks to a software Developer

#38

Post by matt4077 » Thu, Apr 18, 2019, 9:23 PM UTC

HankB99 wrote: post #17

I'm unclear on how moving the engine up causes application of power to cause the attitude to tend to go nose up. I would expect the opposite to happen. I think something else must have changed such as the center line of the engine relative to the center line of the plane. Or did moving the engine forward at the same time cause this effect?

Forward, where the wing is higher off the ground. The rest is like a skateboard suddenly accelerating, which will tend to pitch you nose up (and on the ground).

Re: How the Boeing 737 Max disaster looks to a software Developer

#39

Post by Declanomous » Thu, Apr 18, 2019, 9:23 PM UTC

laydn wrote: post #32

The article states: "When MCAS senses that the angle of attack is too high, it commands the aircraft’s trim system to lower the nose. It also does something else: It pushes the pilot’s control columns downward " No, it does not push the pilot's control columns downward.

I think that the author is mistaking the fact that trimming the plane forward means that more force is required to pull back on the yoke for the plane actively pushing the yoke forward.

Re: How the Boeing 737 Max disaster looks to a software Developer

#40

Post by Declanomous » Thu, Apr 18, 2019, 9:26 PM UTC

HankB99 wrote: post #17

I'm unclear on how moving the engine up causes application of power to cause the attitude to tend to go nose up. I would expect the opposite to happen. I think something else must have changed such as the center line of the engine relative to the center line of the plane. Or did moving the engine forward at the same time cause this effect?

The new engine is more powerful, and at high angles of attack the nacelles also generate lift. The added power, along with the greater displacement from the center of lift/drag causes the plane to pitch up more easily, and the lift from the nacelle causes the controls to get lighter as you approach stall speed.

The FAA requires the controls to get heavier as you approach a stall. MCAS was primarily designed to address this flaw, which is why the added lift from the nacelles is an issue.