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

111–120 of 126 posts

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

#111

Post by feanaro »

compiler-guy wrote: post #96
feanaro wrote: post #28

Earlier quoted context omitted.

> This is a good reason to link to the actual publication source instead of to a PDF copy of the paper (unless you have good reason not to, such as a paywall). It would still be best to include the date inside the artifact itself instead of relying on external and contextual metadata like you are describing. As long as we're at it, documents should also ideally include their DOI.

1996 predates most of the web as we know it today. It was a different time with different standards.

I agree. My comment wasn't about shaming the old standards but about establishing new ones.

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

#112

Post by raverbashing »

jillesvangurp wrote: post #89

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 the…

Uncle Bob is insufferable and thinks that anything less than 100% testing and your code doesn't work.

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

Or you could actually use the software. You can have 100% unit tests passing and a completely broken integration.

He's not exactly wrong in that analogy but I think that in practice such utopia does not exist.

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

#113

Post by galkk »

tester34 wrote: post #106
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 v…

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

I don't think that you need that clarification. The greed of many game developers doesn't have any borders. Artificial delays that force you to spend money to work around them, ridiculous drop rates etc - I, personally, would never judge badly someone who bots, if its doesn't affect other players.

Cheating (such as aimbots, wallhacks, radars, nethacks etc) is totally different story though

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

#114

Post by jondubois »

Formal proofs are useless because most systems in the real world are far too complex to be formally verified. The formal proofs for most systems would be so long and complex that they would be almost guaranteed to suffer from human error; the proofs are much more likely to have errors than the underlying code itself.

It is a tool invented by bureaucrats for the sole purpose of job creation.

If society keeps becoming more bureaucratic, soon enough, someone will invent the concept of unit testing for formal proofs... There is no limit to how ridiculous this can get. The Fed's mandate is job creation, and job creation is just what it'll do! Any job! Mostly useless jobs!

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

#115

Post by swiley »

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.

Correct software has surprisingly little business value.

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

#116

Post by jillesvangurp »

raverbashing wrote: post #112
jillesvangurp wrote: post #89

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 the…

Uncle Bob is insufferable and thinks that anything less than 100% testing and your code doesn't work. > 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. Or you could actually use the software. You can have 100% unit tests passing and a completely broken integration. He's not exactly wrong in that analogy but I think that in practice such…

I'm not advocating TDD either. But he has a point that testing (manual or automated), or even just using the software is a form of experimentation and thus a perfectly valid and scientific way of assessing whether software works or not.

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

#117

Post by 77pt77 »

jolux wrote: post #26
ErikAugust wrote: post #22

Earlier quoted context omitted.

This would be more in the context of FOSS, so the economics are certainly different. I am not sure qualified eyeballs are expensive in this context.

Look at OpenSSL and Heartbleed. Nobody found it and it ended up being a catastrophe. It has since seen major industry investment. The problems have been mostly alleviated.

Anyone worth their salt that spent longer than 10 minutes lokoing at openssl's source code knew that it was riddled with problems.

Regardless of that none of the many billion dollar companies that relied on it invested anything into improving it.

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

#118

Post by 77pt77 »

mamon wrote: post #40
ErikAugust wrote: post #4

One thing I would think helps software is Linus's law: "Given enough eyeballs, all bugs are shallow". https://en.wikipedia.org/wiki/Linus%27s_law As far as I know, this is not something available to other forms of engineering.

"No one reads anything. Those who do read, they do not understand. Those who do understand, they immediately forget." "Linus's law" is refered to as "Linus's fallacy" now.

And the ones that don't forget eventually get discouraged by having to go through people like him.

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

#119

Post by viluon »

doonesbury wrote: post #79
MR4D wrote: post #73

Natural Selection. If you account for survivorship bias, I would bet that software is not very reliable.

Agree. Plus plenty of labor has gone into customer facing bugs that autos, hw, consumer electronics etc prob wouldn't stand for. And we build on hw which is formally verified.

> And we build on hw which is formally verified.

Ehm, what?

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

#120

Post by Jtsummers »

viluon wrote: post #119
doonesbury wrote: post #79

Earlier quoted context omitted.

Agree. Plus plenty of labor has gone into customer facing bugs that autos, hw, consumer electronics etc prob wouldn't stand for. And we build on hw which is formally verified.

> And we build on hw which is formally verified. Ehm, what?

Intel (and presumably others) use formal methods to verify their hardware designs, or at least large portions of them. This started in earnest after the FDIV bug. Here's a presentation on the topic (dated now, but my understanding is the use of formal methods has only increased since then).

https://www.cl.cam.ac.uk/~jrh13/slides/nijmegen-21jun02/slid...

Post reply on HN