Hacker News Reader

Comment by just_steve_h | Hacker News Reader

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.

View on HN

There have been attempts (the "Keep the Space Shuttle Flying" method): https://github.com/kubernetes/kubernetes/blob/ec2e767e593953...

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.

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.

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.

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.

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.

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.

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

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

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.

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.

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)

I think being able to prove that a program can be correct is getting close to P=NP territory.

It's very difficult but there have been strides in that direction: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....

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.

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.

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?

Reply on news.ycombinator.com