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

How Did Software Get So Reliable Without Proof? (1996) [pdf]

gwern.net

Post reply on HN
Print view View original

81–90 of 126 posts

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#81

Post by ahelwer »

chas wrote: post #64
disown wrote: post #54

Because reliable and proof are not the same concepts and one is not needed for the other. Proof is logical certainty for all time ( in the past, present and future ). Reliability is not. Reliability doesn't require mathematical proof - this goes for airplanes to your kitchen faucet to software. Software became more and more reliable through testing, errors, fixes/patches, etc. Also, many times good enough is good eno…

The control systems for airplanes often have a significant number of mathematical proofs.

Formal methods aren't as widespread in safety critical industries as you might hope or believe. Model-based testing is still considered cutting edge, never mind formal verification.

Formal verification is only as good as your model, anyway. Problem comes from outside your model? Formal verification won't save you.

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#82

Post by redis_mlc »

hcarvalhoalves wrote: post #15

It didn't - but most errors are simply tolerated because imperfect automation still has absurd economy of scale, very few applications are on a regulated field or have a well-defined quality standard to meet, and unreliable software tends to at least fail consistently, so it's still a win to diagnose and fix processes compared to humans making creative mistakes.

Well, actually it did.

Some of the reasons are:

1) Most applications use very reliable databases as a store. Back in the day, programmers used to write their own one-off BTREE libraries, which stopped with msql/mysql, jet, dbm and sqlite.

(A holdover from that era is when interviewers asked you to roll your own sort algorithm, which you should almost never do for production apps.)

2) Some software is fuzzed.

3) Some software has managed memory.

4) Some software has tests.

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#83

Post by 6nf »

war1025 wrote: post #80
chas wrote: post #64

Earlier quoted context omitted.

The control systems for airplanes often have a significant number of mathematical proofs.

My father-in-law works on control systems for airplanes and I get the impression that it's based much more on testing in flight simulators than on any amount of proofs. The level he works at might be higher level though. It sounds like control systems for airplanes are fairly modular.

Donald Knuth quote: Beware of bugs in the above code; I have only proved it correct, not tried it.

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#84

Post by Jtsummers »

AnimalMuppet wrote: post #51

First: Software got so abundant without proof. How much of an effort is a formal proof of a program? I suspect that it's at least as much effort as the total effort of writing the program, and maybe several times that. If I'm right, then formally proving all programs would result in more than twice as much effort, which would mean less than half as much software. So, think of all the programs that you interact with i…

> First: Software got so abundant without proof. How much of an effort is a formal proof of a program? I suspect that it's at least as much effort as the total effort of writing the program, and maybe several times that. If I'm right, then formally proving all programs would result in more than twice as much effort, which would mean less than half as much software. So, think of all the programs that you interact with in a day. Now think of a world where half of those programs simply do not exist. Is that better than this world of buggy programs? Or worse?

I don't think it'd require twice the effort unless you insisted on a full and complete formal proof of the entire program. Which most contemporary advocates of formal methods do not want (and this paper basically concurs with). Rather, see TLA+ where the advocation is for people to model critical parts, or the concurrency model, or the synchronization model of their distributed system. You can elide so many details that it's nowhere near the same level of work as actually writing the full program, but can inform your design so that you spend less time reworking later.

OTOH, I've seen lots of programs where the testing comprises at least as much effort, if not some small integer multiple, as the actual coding portion. But no one is advocating for removing tests (though some people strongly despise, if not outright hate, certain test approaches).

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#86

Post by AnimalMuppet »

Jtsummers wrote: post #84
AnimalMuppet wrote: post #51

First: Software got so abundant without proof. How much of an effort is a formal proof of a program? I suspect that it's at least as much effort as the total effort of writing the program, and maybe several times that. If I'm right, then formally proving all programs would result in more than twice as much effort, which would mean less than half as much software. So, think of all the programs that you interact with i…

> First: Software got so abundant without proof. How much of an effort is a formal proof of a program? I suspect that it's at least as much effort as the total effort of writing the program, and maybe several times that. If I'm right, then formally proving all programs would result in more than twice as much effort, which would mean less than half as much software. So, think of all the programs that you interact with…

Fair.

OTOH, the less you prove correct, the more bugs you leave, and you get people asking "How did software get so reliable with so little proof?"

On the third hand (I think that's the number I'm up to now), types are a kind of proof, and I really do want those. So I think there's some kind of curve, with no proof giving you lots of bugs (which are expensive to fix, and bad for your product's PR), and full proof taking forever and costing a ton, and somewhere in between being the sweet spot.

And where is that sweet spot? I would say at least type systems, but less than full formal proof. Somewhere in between, which leaves a lot of room and therefore is not much help. Worse, where exactly the sweet spot is probably depends on several things, which means we can't give any simple answer.

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#87

Post by 6nf »

thereisnospork wrote: post #68
chas wrote: post #64

Earlier quoted context omitted.

The control systems for airplanes often have a significant number of mathematical proofs.

The bolts don't, and yet they don't (usually) fail.

Every single bolt on a plane is tracked from the steel foundry to retirement with serial numbers and testing and certification and everything.

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#89

Post by jillesvangurp »

Uncle Bob makes some interesting points about software testing and scientific methodology. His main point is that science is mostly not about proving things correct but about attempting to find ways to falsify an hypothesis by doing experiments. Failing to do falsify means the hypothesis is more likely to be true at some level. It could still be wrong or imperfect and theories are often refined or replaced by new theories. Science is about trying to find ways to prove things wrong and occasionally failing to do that in interesting ways. The more you fail at that, the better a theory becomes. If you succeed (by failing), you refine your theory and run more experiments.

Software testing is exactly the same. The more tests you have, the more evidence you build up that the theory that the software is incorrect in some way may be wrong. If you find out about a new way it could still be wrong, you write a test to prove that wrong. And then if you are right about that, you fix the software.

Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]

#90

Post by hyperman1 »

lmilcin wrote: post #47

I think the reason is natural selection. Since the beginning of computer software (and computer hardware) the solutions that were not reliable enough for practical purposes were discarded.

I've seen a paper provide a natural selection model of bugs: If a bug occurs frequently enough, someone will bother to fix it.

Hence, popular software has less bugs and becomes more popular. Using popular software in a different way will trigger unfound bugs.

Security bugs were special, as nobody triggers them by default. There is no selection pressure to make them disappear.

Post reply on HN