Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

How the Boeing 737 Max disaster looks to a software Developer

spectrum.ieee.org

Post reply on HN
Print view View original

21–30 of 306 posts

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

#21

Post by rightbyte »

scrape_it wrote: post #11
crimsonalucard wrote: post #7

Earlier quoted context omitted.

No, I get it, but still... it's ironic. Software for a plane, though, I would want 1% code 99% proofs.

Well, to support the top parent's comment, here's what John Carmack had to say about SAAB's fighter jet: > The fly-by-wire flight software for the Saab Gripen (a lightweight fighter) went a step further. It disallowed both subroutine calls and backward branches, except for the one at the bottom of the main loop. Control flow went forward only. Sometimes one piece of code had to leave a note for a later piece telling…

Interesting about the SAAB fighter. Essentially the opposite of spaghetti code? One really long spaghetti straw that is uncooked?

I like really long function bodys so I get turned on by the idea.

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

#22

Post by WalterBright »

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.

Proving that software matches the spec is one thing, proving that the spec is free of bugs is quite another.

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

#23

Post by samatman »

alacombe wrote: post #10
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.

Proving something is correct is only part of the problem. A random bit flip (no matter amount of error correction and physical hardening) and your proven-correct software goes amok. And this is just one of the many issue you can encounter dealing with the physical world.

Ironically, the solution to this in spacecraft, where radiation is a given, is 2 of 3 with polling.

The system which should have been using for attitude detection in the 737 MAX, and wasn't.

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

#24

Post by throwaway2048 »

crimsonalucard wrote: post #14
softwaredoug wrote: post #8

Earlier quoted context omitted.

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.

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

#25

Post by fwip »

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?

They moved it forward so they could move it up, but the centerline of the engine was still under the original engine's centerline.

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

#26

Post by leoedin »

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?

I don't think it does. Other sources I've read suggest the larger nacelle introduces a pitch up during certain flap configurations and at a high angle of attack. It's not the engine thrust that's the problem, but the drag due to the large and further forward nacelle. That's the justification for the MCAS software.

https://theaircurrent.com/aviation-safety/what-is-the-boeing...

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

#27

Post by throwaway2048 »

samatman wrote: post #23
alacombe wrote: post #10

Earlier quoted context omitted.

Proving something is correct is only part of the problem. A random bit flip (no matter amount of error correction and physical hardening) and your proven-correct software goes amok. And this is just one of the many issue you can encounter dealing with the physical world.

Ironically, the solution to this in spacecraft, where radiation is a given, is 2 of 3 with polling. The system which should have been using for attitude detection in the 737 MAX, and wasn't.

Dosen't eliminate a single point of failure, after all a bitflip in the voting mechanism can also result in error.

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

#28

Post by scrape_it »

mongol wrote: post #20
scrape_it wrote: post #11

Earlier quoted context omitted.

Well, to support the top parent's comment, here's what John Carmack had to say about SAAB's fighter jet: > The fly-by-wire flight software for the Saab Gripen (a lightweight fighter) went a step further. It disallowed both subroutine calls and backward branches, except for the one at the bottom of the main loop. Control flow went forward only. Sometimes one piece of code had to leave a note for a later piece telling…

Interesting quote. Seems it was actually a quote of Henry Spencer by Carmack. http://number-none.com/blow/john_carmack_on_inlined_code.htm... Note however that there were several software-related crashes in the early days of Gripen. Might not be related to exactly this code, but to the problem of regulating the feedback loops to manage the plane's purposeful instability

huh? interesting, do you have more info, I love reading stuff like this. I don't know much about the Gripen but it is my all time favorite after the F-16.

Off topic but here's a neat youtube video of Gripen jets undergoing rapid turn-around, on a normal street road with just a handful of people, and special tools for the crew:

https://www.youtube.com/watch?v=49L9BlYQSjw

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

#29

Post by umvi »

bollu wrote: post #5
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'm not sure you understand how difficult it is to prove software correct. I've written a decent amount of Coq code. It's quite bonkers how much of proof one needs to write to get anything done. For reference, the certified compiler CompCert's code base is something like 10% code and 90% proofs.

Even then it doesn't matter if your software is "correct" if you don't understand/have not captured all the requirements.

You could write a formally verified MCAS system in Coq or whatever that still kills people because you didn't consider the case of sensor failure (because that wasn't in the requirements). Or because you didn't consider the case of double sensor failure or a combination of extremely rare hardware failures (that wasn't in the requirements either!).

Your code is mathematically perfect, yes! But it was built with the incorrect assumption that the hardware is perfect as well!

I'll take a robust set of tests written by someone thinking outside of the box in terms of what could fail, how it will be used in operation, etc. over a piece of software "guaranteed unsinkable" because it is formally verified.

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

#30

Post by mikeash »

tluyben2 wrote: post #15
bollu wrote: post #5

Earlier quoted context omitted.

I'm not sure you understand how difficult it is to prove software correct. I've written a decent amount of Coq code. It's quite bonkers how much of proof one needs to write to get anything done. For reference, the certified compiler CompCert's code base is something like 10% code and 90% proofs.

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” and ended up with the exact same result.

A lot of software problems are due to discrepancies between the design and the implementation, of course. But it’s not a panacea.

Post reply on HN