How the Boeing 737 Max disaster looks to a software Developer
spectrum.ieee.org
How the Boeing 737 Max disaster looks to a software Developer
1–10 of 306 posts
Re: How the Boeing 737 Max disaster looks to a software Developer
#2The 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.
Re: How the Boeing 737 Max disaster looks to a software Developer
#3The 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.
Well we can prove some things behave under certain conditions in a certain way. We can't prove the absence of bugs.
Re: How the Boeing 737 Max disaster looks to a software Developer
#4The 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.
Isn't digital logic testing a thing for hardware?
Re: How the Boeing 737 Max disaster looks to a software Developer
#5The 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.
Re: How the Boeing 737 Max disaster looks to a software Developer
#6The 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.
Well we can prove some things behave under certain conditions in a certain way. We can't prove the absence of bugs.
No, we can literally prove it correct based off of a specification.
https://en.wikipedia.org/wiki/Correctness_(computer_science)
In science nothing can be proven but in the world of logics and math, things can be proven. Bugs can arise where programs intersect in the real world.
Re: How the Boeing 737 Max disaster looks to a software Developer
#7The 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.
No, I get it, but still... it's ironic. Software for a plane, though, I would want 1% code 99% proofs.
Re: How the Boeing 737 Max disaster looks to a software Developer
#8Earlier quoted context omitted.
Well we can prove some things behave under certain conditions in a certain way. We can't prove the absence of bugs.
No, we can literally prove it correct based off of a specification. https://en.wikipedia.org/wiki/Correctness_(computer_science) In science nothing can be proven but in the world of logics and math, things can be proven. Bugs can arise where programs intersect in the real world.
Yeah and then the specification at that level of specificity IS the code. How do you prove the specification is bug free?
Re: How the Boeing 737 Max disaster looks to a software Developer
#9What 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.
Re: How the Boeing 737 Max disaster looks to a software Developer
#10The 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.