5 ms·

I worked at a Large Internet Infrastructure Company for a long time, and saw software development practices that made my hair curl. All I could think was, "Gee,

I worked at a Large Internet Infrastructure Company for a long time, and saw software development practices that made my hair curl. All I could think was, "Gee, I'm glad we're not working on aviation software!" Seriously, though: software "engineering" could actually earn the name, if we had rigorous professional standards, regulatory oversight, and product liability.

Dirlewanger 6y ago
One thing that sets software apart from other engineering disciplines is that they are grounded in physics (bits running on a semiconductor doesn't matter for this discussion) and have been around (in some form) for thousands of years. How do we know if a design is sound? We can check it by doing the math. How do we know if a program is sound (what does that even mean? There's our first problem)? Well, we rely on a large compendium of heuristics that are based on nothing but experiences compiled over the past ~60 years. Also, that compendium is constantly being added to. Also, virtually everyone disagrees on what should/shouldn't be in this compendium.
- just_steve_h 6y ago
  I'm wading into waters that are way over my head here, but my understanding is that it is possible for software to be provably correct, in the mathematical sense of "proof." I'm well aware of the admixture of folklore, experience, and caffeine-fueled inspiration that constitutes much of the software that runs our world.
  - ghaff 6y ago
    There's work going on in formal verification but it has many limitations. I'd also point out that in MechE/CivE fields, you're still dependent on materials (and maintenance) working as advertised. It's also often the case that operating conditions just end up being different from what was designed for or certain failure modes weren't considered. See, e.g. the Citibank Building in NYC http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_tower_design_flaw_that_could_have_wiped_out_the_skyscraper.html http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_t...
  - vvanders 6y ago
    Have a peek a metastability[1], any time a digital system crosses a clock domain there's basically statistics making sure the whole thing doesn't fall over. From need a better MTBF? Throw a couple more inline flip-flops. [1] https://en.m.wikipedia.org/wiki/Metastability_(electronics) https://en.m.wikipedia.org/wiki/Metastability_(electronics)
  - Dirlewanger 6y ago
    I think being able to prove that a program can be correct is getting close to P=NP territory.
    - Raptor22 6y ago
      It's very difficult but there have been strides in that direction: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....
    - aklein 6y ago
      Cannot prove some program is correct, in general, because that’s effectively the halting problem. But in practice it is sufficient to enforce (prove) the absence of behaviors via constraints like types or contracts.
  - bluGill 6y ago
    You can, but first we need to figure out what correct is in the first place. I can prove hello world doesn't overflow buffers, but it is a bit harder to prove that my font renders the letters vs some random scribbles.
  - rocqua 6y ago
    It is possible to prove software adheres to a certain specification. This is time consuming, and how feasible it is depends a lot on how your specification was written. It generally also depends on how your software was written. The big issue is that writing a useful specification can be hard. Especially if you want to also make the specification easy to check. A side issue is that your proof will make assumptions about how a computer works that are simplified.
  - archi42 6y ago
    Source: I work on static analyzers, so I'm biased to that. We can not prove everything, as others pointed out the fundamental issue here is the "halting problem". However, this doesn't mean we can't prove anything. Wikipedia says: > In computability theory, Rice's theorem states that all non-trivial, semantic properties of programs are undecidable. I often feel like the "trick" is to push the trivial stuff to be as useful as possible. You can work from several vectors: 1. You build better static analyzers (difficult and computationally expensive the further you push it - but that's what we're doing) 2. reduce the complexity of the "analyzed thing" (high level language, assembly,...) to allow for easier analysis, while still being useful (a assembly language only supporting 'nop' is trivial to analyze, but pretty useless overall; otoh you can disallow some constructs in C to make the language easier to analyze). There are of course other forms of "provably correct". E.g. programming in a language that has proofs attached to it, like coq [which is the name of a proof assistant]. Disclaimer: I've never used coq myself, but know plenty who do. I think that's something that might interest you. [And thanks to the genius who christened that tool: No, seriously, I'm not trying to be rude!] [edit] Didn't check that link, but maybe you find it interesting https://www.cs.princeton.edu/courses/archive/spring13/cos510/sf/Basics.html https://www.cs.princeton.edu/courses/archive/spring13/cos510... There are of course other approaches than coq, e.g. Isabelle is often mentioned. See the "See also" on https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq
hu3 6y ago
General software requirements can change drastically in a short period. Heck one of our clients requested major parts of our solution to be rebuilt for the third time within 6 months to accommodate the whims of their new leadership. You don't see that happening with aviation software where requirements are set in stone.
- starpilot 6y ago
  So raise the price of the software so that you can afford more/better software engineers, to produce a more robust and flexible project. Then it'll be aerospace quality, aerospace costs.
  - hu3 6y ago
    So your solution is to charge more and throw more engineers at the problem? Sounds like one of my ex-bosses. Apple does that and they couldn't be further apart from aerospace engineering quality. Their software and hardware has been historically littered with problems and bugs.
da_big_ghey 6y ago
Exists for these reasons secure coding standards, MISRA and BARR and others. If we had same restrictions as other engineering profession maybe we still use COBOL. In important places with big safety concern we follow better guidelines, in webshit front end are do more, not so much concern with a mistaking. This is the best way, the allow of breaking in unimportant but make rule in important.
starpilot 6y ago
You just don't need that in software when most of the industry is low consequence. It's only losing money at most tech companies, not killing your coworkers. This hasn't happened to me personally, but it's not cool when Rob the test pilot, whose family you've hung out with and that you've gone on hikes with, literally dies next day in a fiery crash. But that's the risk any test pilot accepts.
- just_steve_h 6y ago
  That's the excuse I keep heading. Then, I find out that the "low consequence" software I've worked on is being relied upon in very consequential contexts. Can I tell your customers that the software you're selling them is only built for "low consequence" applications?
stareatgoats 6y ago
There have been attempts (the "Keep the Space Shuttle Flying" method): https://github.com/kubernetes/kubernetes/blob/ec2e767e59395376fa191d7c56a74f53936b7653/pkg/controller/volume/persistentvolume/pv_controller.go https://github.com/kubernetes/kubernetes/blob/ec2e767e593953...

Dirlewanger 6y ago

One thing that sets software apart from other engineering disciplines is that they are grounded in physics (bits running on a semiconductor doesn't matter for this discussion) and have been around (in some form) for thousands of years. How do we know if a design is sound? We can check it by doing the math. How do we know if a program is sound (what does that even mean? There's our first problem)? Well, we rely on a large compendium of heuristics that are based on nothing but experiences compiled over the past ~60 years. Also, that compendium is constantly being added to. Also, virtually everyone disagrees on what should/shouldn't be in this compendium.

just_steve_h 6y ago
I'm wading into waters that are way over my head here, but my understanding is that it is possible for software to be provably correct, in the mathematical sense of "proof." I'm well aware of the admixture of folklore, experience, and caffeine-fueled inspiration that constitutes much of the software that runs our world.
- ghaff 6y ago
  There's work going on in formal verification but it has many limitations. I'd also point out that in MechE/CivE fields, you're still dependent on materials (and maintenance) working as advertised. It's also often the case that operating conditions just end up being different from what was designed for or certain failure modes weren't considered. See, e.g. the Citibank Building in NYC http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_tower_design_flaw_that_could_have_wiped_out_the_skyscraper.html http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_t...
- vvanders 6y ago
  Have a peek a metastability[1], any time a digital system crosses a clock domain there's basically statistics making sure the whole thing doesn't fall over. From need a better MTBF? Throw a couple more inline flip-flops. [1] https://en.m.wikipedia.org/wiki/Metastability_(electronics) https://en.m.wikipedia.org/wiki/Metastability_(electronics)
- Dirlewanger 6y ago
  I think being able to prove that a program can be correct is getting close to P=NP territory.
  - Raptor22 6y ago
    It's very difficult but there have been strides in that direction: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....
  - aklein 6y ago
    Cannot prove some program is correct, in general, because that’s effectively the halting problem. But in practice it is sufficient to enforce (prove) the absence of behaviors via constraints like types or contracts.
- bluGill 6y ago
  You can, but first we need to figure out what correct is in the first place. I can prove hello world doesn't overflow buffers, but it is a bit harder to prove that my font renders the letters vs some random scribbles.
- rocqua 6y ago
  It is possible to prove software adheres to a certain specification. This is time consuming, and how feasible it is depends a lot on how your specification was written. It generally also depends on how your software was written. The big issue is that writing a useful specification can be hard. Especially if you want to also make the specification easy to check. A side issue is that your proof will make assumptions about how a computer works that are simplified.
- archi42 6y ago
  Source: I work on static analyzers, so I'm biased to that. We can not prove everything, as others pointed out the fundamental issue here is the "halting problem". However, this doesn't mean we can't prove anything. Wikipedia says: > In computability theory, Rice's theorem states that all non-trivial, semantic properties of programs are undecidable. I often feel like the "trick" is to push the trivial stuff to be as useful as possible. You can work from several vectors: 1. You build better static analyzers (difficult and computationally expensive the further you push it - but that's what we're doing) 2. reduce the complexity of the "analyzed thing" (high level language, assembly,...) to allow for easier analysis, while still being useful (a assembly language only supporting 'nop' is trivial to analyze, but pretty useless overall; otoh you can disallow some constructs in C to make the language easier to analyze). There are of course other forms of "provably correct". E.g. programming in a language that has proofs attached to it, like coq [which is the name of a proof assistant]. Disclaimer: I've never used coq myself, but know plenty who do. I think that's something that might interest you. [And thanks to the genius who christened that tool: No, seriously, I'm not trying to be rude!] [edit] Didn't check that link, but maybe you find it interesting https://www.cs.princeton.edu/courses/archive/spring13/cos510/sf/Basics.html https://www.cs.princeton.edu/courses/archive/spring13/cos510... There are of course other approaches than coq, e.g. Isabelle is often mentioned. See the "See also" on https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq

hu3 6y ago

General software requirements can change drastically in a short period. Heck one of our clients requested major parts of our solution to be rebuilt for the third time within 6 months to accommodate the whims of their new leadership. You don't see that happening with aviation software where requirements are set in stone.

starpilot 6y ago
So raise the price of the software so that you can afford more/better software engineers, to produce a more robust and flexible project. Then it'll be aerospace quality, aerospace costs.
- hu3 6y ago
  So your solution is to charge more and throw more engineers at the problem? Sounds like one of my ex-bosses. Apple does that and they couldn't be further apart from aerospace engineering quality. Their software and hardware has been historically littered with problems and bugs.

da_big_ghey 6y ago

Exists for these reasons secure coding standards, MISRA and BARR and others. If we had same restrictions as other engineering profession maybe we still use COBOL. In important places with big safety concern we follow better guidelines, in webshit front end are do more, not so much concern with a mistaking. This is the best way, the allow of breaking in unimportant but make rule in important.

starpilot 6y ago

You just don't need that in software when most of the industry is low consequence. It's only losing money at most tech companies, not killing your coworkers. This hasn't happened to me personally, but it's not cool when Rob the test pilot, whose family you've hung out with and that you've gone on hikes with, literally dies next day in a fiery crash. But that's the risk any test pilot accepts.

just_steve_h 6y ago
That's the excuse I keep heading. Then, I find out that the "low consequence" software I've worked on is being relied upon in very consequential contexts. Can I tell your customers that the software you're selling them is only built for "low consequence" applications?

stareatgoats 6y ago

There have been attempts (the "Keep the Space Shuttle Flying" method): https://github.com/kubernetes/kubernetes/blob/ec2e767e59395376fa191d7c56a74f53936b7653/pkg/controller/volume/persistentvolume/pv_controller.go https://github.com/kubernetes/kubernetes/blob/ec2e767e593953...