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

101–110 of 126 posts

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

#101

Post by TheUndead96 »

doteka wrote: post #97
johnisgood wrote: post #92

Earlier quoted context omitted.

5) Some software is formally verified Formal verification is huge these days I would like to think.

Huge? I have worked in this industry for a while now and never heard anyone outside of HN even mention it. It’s decidedly not huge for any definition of huge (outside of academia maybe?)

The "big production" example that kept being referred to in university was a (Belgian?) metro system. I think it was well suited to formal verification because it had a finite number of valid states, and the cost of failure was sufficient to justify the investment.

EDIT: I now think it was French, source https://www.prover.com/portfolio-items/ratp-paris/

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

#102

Post by dehrmann »

ookdatnog wrote: post #93
dehrmann wrote: post #74

Earlier quoted context omitted.

I'm not sure if that's a victory or a loss for formal proofs. Sure, it found the bug, but for a language that popular, it wasn't a very meaningful bug, and sorting algorithms is one of the easier things to analyze.

For algorithms without provided proof, we can only estimate their correctness based on how battle-tested they are. If an algorithm has been run many times and it has been correct every one of those times, then we feel somewhat confident that we got it right. Over time, we'll find weird edge cases where it doesn't work, and fix them. Few algorithms are as battle-tested as the sorting algorithm from the Java standard l…

> even software that's this battle-tested is still not fully reliable

But does it matter?

I also don't understand formal methods well, but wouldn't they also be subject to bugs? It seems like all we can do is make software less unreliable.

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

#103

Post by roenxi »

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.

If it is possible to use proof that is lovely; but it isn't necessary. Things have been engineered to very high levels of reliability with only the most tangential reliance on proofs.

Software is highly unusual in that proofs can even be deployed. Most highly safe processes can't even use proofs. How do you prove that a dam won't fail? It is impossible.

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

#104

Post by lecunn »

doteka wrote: post #97
johnisgood wrote: post #92

Earlier quoted context omitted.

5) Some software is formally verified Formal verification is huge these days I would like to think.

Huge? I have worked in this industry for a while now and never heard anyone outside of HN even mention it. It’s decidedly not huge for any definition of huge (outside of academia maybe?)

https://aws.amazon.com/security/provable-security/?nc1=h_ls

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

#105

Post by tehjoker »

redis_mlc wrote: post #82
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…

There was this item on HN recently. :)

https://probablydance.com/2016/12/27/i-wrote-a-faster-sortin...

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

#106

Post by tester34 »

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.

> because imperfect automation still has absurd economy of scale

That's what FULL AFK botting in games taught me, kinda random % values, so in my experience it was

Automating 80% of stuff is easy, can be done in 1h

90% is starting getting tricky

95% requires you to spend days of testing and writting various scripts

100% is additionally limited by BOT API and would require you to write your own stuff and talk to bot via e.g file system and try to handle things like client/bot crashes, networking maybe, damn...

But yea, having to do something once a day for 10min instead of playing 10h is great enough

Just to clarify: those are private servers where everybody's botting.

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

#107

Post by twblalock »

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.

The other major factor is fault tolerance. Software has bugs, and hardware breaks, but that's accepted. Programmers in industry have invested a lot of time in routing around the problems. That buys time for human operators to get paged and fix things.

For every major outage that makes the news, there are thousands of smaller problems that users never notice because of CDNs, failover, graceful-ish service degradation, autoscaling and/or overprovisioning, and fallbacks. Services can be reliable even when the software and hardware that backs them is not.

In other words, "reliability" is a property of the whole system, including the human operators, not just the code. The code can actually be pretty bad, yet the entire system can still be reliable in terms of being available and functional when the users want to use it.

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

#108

Post by deckplecksetter »

doteka wrote: post #97
johnisgood wrote: post #92

Earlier quoted context omitted.

5) Some software is formally verified Formal verification is huge these days I would like to think.

Huge? I have worked in this industry for a while now and never heard anyone outside of HN even mention it. It’s decidedly not huge for any definition of huge (outside of academia maybe?)

It's used to some extent in the aviation industry for flight-critical software. So maybe huge in some contexts.

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

#109

Post by MaxBarraclough »

xmprt wrote: post #60
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…

Proofs are only valid as long as the requirements don't change and assumptions are still valid. Two things that any first year CS student could tell you are absurd to even imagine.

You seem to be dismissing formal methods, but they've been used successfully in various domains.

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

#110

Post by lmilcin »

hyperman1 wrote: post #90
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.

I think of bugs as signal.

Bugs are energy of noise on continuous spectrum where frequency describes types of bugs.

When you write software you generate initial signal which will depend on what you are doing and your ability (awareness of different types of bugs, etc.)

Then during further stages of testing these bugs tend to be filtered out. Some types of bugs are attenuated very efficiently. For example a bug that would cause your application to not compile would have very little chance of being shipped...

Some bugs are only detected (as signal) only in some circumstances. For example, users use a detector that has different characteristics from the detector used by developer.

You don't generally want to invest in attenuating all frequencies. What you do is you ignore frequencies that don't matter (that just pass and cause no harm) and focus on harmful frequencies.

In the end, the best way to reduce the output noise of the system is usually to reduce the input noise (ie. signal produced by developer).

Post reply on HN