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

51–60 of 306 posts

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

#51

Post by stefan_ »

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.

It also makes absolutely no sense in any software that works entirely with and relies on external, mechanical hardware sensors. There is a reason people use this to certify their operating system or algorithm works: you can forever stay in a bubble that your processor is just a big math machine, no external inputs, no external outputs. We have "certified secure" operating systems that nonetheless are trivially attacked through something like rowhammer.

How do you solve it? Assume your AoA sensor is always correct? Congratulations, MCAS is a provably correct solution! Make the sensor behavior more complex? Sorry, the problem is now intractably complex (and still doesn't model the actual hardware).

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

#52

Post by uxp100 »

wpietri wrote: post #16
wpietri wrote: post #9

What a stellar example of an article on a complex topic written to be clear enough for the audience to understand. I especially like the way he brought it back repeatedly to hands out the window and bitey dogs.

I also heartily agree with him that software's general laxity with regards to reliability is contagious. I've come think that calling it all "software" is dangerous, like thinking of all things made with atoms as the same. I think we as an industry should get together, divide the work into various domains, and establish professional and ethical standards for the domains that matter. Standards with teeth, such that de…

I don't know that this hasn't been done already. If you're working on automotive software, for example, you will comply with ISO 26262. Is this the type of professional standards you are referring to?

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

#54

Post by digikata »

paulopontesm wrote: post #34
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...

I suspect combined reliability of a simple switch and two independent systems is likely higher than one composite system and pilots or software trying to estimate and select which combinations of computers & sensors are "good" in the middle of an emergency.

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

#55

Post by rubicon33 »

rkagerer wrote: post #49

I believe the relative ease — not to mention the lack of tangible cost — of software updates has created a cultural laziness within the software engineering community. -- This --^ As someone who carefully crafts their code to strive for perfection, seeing sloppy work out there in the wild drives me nuts. I know folks here will deride me for being "inefficient", but in the long term I still maintain from my experience…

If only managers and CEOs saw it the same way.

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

#56

Post by teddyh »

nextos wrote: post #42
teddyh wrote: post #31

Earlier quoted context omitted.

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 th…

I have a MSc in formal methods, and this is really misleading. Surely you cannot make some proofs easily. However, how did Airbus verify that some errors simply do not exist in their fly-by-wire software (which is ~100 KLOC implemented in a subset of C)? (I'm sure Boeing also employs these techniques internally). Using abstract interpretation. There are tons of formal methods, ranging from type systems to formal proo…

I wonder if anyone can follow Feynman’s style of proof?

By the end of that summer of 1983, Richard had completed his analysis of the behavior of the router, and much to our surprise and amusement, he presented his answer in the form of a set of partial differential equations. To a physicist this may seem natural, but to a computer designer, treating a set of boolean circuits as a continuous, differentiable system is a bit strange. Feynman's router equations were in terms of variables representing continuous quantities such as “the average number of 1 bits in a message address.” I was much more accustomed to seeing analysis in terms of inductive proof and case analysis than taking the derivative of “the number of 1’s” with respect to time.

http://longnow.org/essays/richard-feynman-connection-machine...

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

#57

Post by chopin »

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…

I don't know about modern systems but PLC's (industrial controllers) worked exactly this way when I worked with them in the 90s. You can introduce subtle bugs with these either.

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

#58

Post by WalterBright »

_bxg1 wrote: post #36

"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.

All engineering designs are full of compromises (the article uses "hacks" meaning compromises), as there are a large number of competing issues at work. Pretty much none of those issues are ever aligned along the same axis.

For just a taste of this, an airliner flies at high altitude, and at low altitude. It flies at low speeds, and high speeds. It flies heavily loaded and empty. Optimizing for any one of these regimes means unacceptable behavior on the others. So compromises are necessary.

Ever notice the flaps on the wings? They're a compromise (a "hack" if you will) to change the shape of the wing to make it work better across different flight regimes. Because metal isn't very flexible, and a long list of other issues with the machinery that operates the flaps, the shape of them is hardly anything but compromises.

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

#59

Post by WalterBright »

nutjob2 wrote: post #41
_bxg1 wrote: post #36

"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.

The modern 737 is a collection of hardware and software hacks, flying in close formation.

So is any airplane that was ever built that is capable of flying.

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

#60

Post by winrid »

rubicon33 wrote: post #55
rkagerer wrote: post #49

I believe the relative ease — not to mention the lack of tangible cost — of software updates has created a cultural laziness within the software engineering community. -- This --^ As someone who carefully crafts their code to strive for perfection, seeing sloppy work out there in the wild drives me nuts. I know folks here will deride me for being "inefficient", but in the long term I still maintain from my experience…

If only managers and CEOs saw it the same way.

At my current company all leadership is in agreement that it is more expensive to deal with bugs in production.
Post reply on HN