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

51–60 of 126 posts

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

#51

Post by AnimalMuppet »

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?

Second: Programs got so reliable by killing the bugs that made them most unreliable. That is, if a program has two bugs, one of which 10% of people hit, and one of which 0.0001% of people hit, the 10% bug gets fixed. The program is still buggy, but it's buggy in a way that most people never encounter.

And third: For (many kinds of) formal proof, you need a formal specification. Much of software is somewhat discovered. (What's the right user interaction flow for this, anyway? Let's try some ideas out and see.) If you write the formal specification before you have really discovered what the software should be, then you can have formally-proven software that does less-than-optimal things.

And then you can have bugs in the specification. (Hello, MCAS!) Formally proving that you correctly implemented an incorrect spec does not make the software more correct.

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

#54

Post by disown »

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 enough. We don't need the perfect for most situations.

Also, it's a subjective call too. For some software is an unreliable mess and we need to throw everything out and rebuild it from scratch. Search for haskell, rust, etc threads. The neverending arguments against side-effects, mutation, pointers, etc. For most, they are good enough and get the job done.

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

#55

Post by _AzMoo »

Animats wrote: post #48
TheOtherHobbes wrote: post #32

Earlier quoted context omitted.

"Given enough projects, all eyeballs are elsewhere."

Yes. Outside of the top 20 or so open source projects, few people are watching. Often only one.

I don't think that's really true. I have open source projects that nobody else actually uses, but I still get messages from people reading and looking at the code. There's often only one person maintaining open source software, but I'd bet there's a lot of eyes on a lot of projects.

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

#56

Post by ben509 »

amelius wrote: post #41
javiramos wrote: post #5

Earlier quoted context omitted.

Definitely true for my domain, mechanical engineering. Enough reviews and bugs will be found and corrected.

Reminds me of the old jokes that start with "if cars were like computers". https://www-users.cs.york.ac.uk/susan/joke/crash.htm

Self-driving cars and IoT turned that joke into prophecy.

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

#57

Post by coldtea »

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.

Unfortunately, we've found out in the subsequent 20+years since that was said, that most projects, even major ones, don't have enough eyeballs...

There was a point a few years ago that GTK+ dev was complaining that only he was left to work on the project. A single person for a whole GUI lib..

And GTK+ is the basis of so many FOSS it's not even funny...

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

#58

Post by stan_rogers »

Jtsummers wrote: post #31
snarkypixel wrote: post #25

Are there any research projects trying to make "proof" programs / languages?

Dependently typed languages may fit what you're asking for. See Idris and the book Type-Driven Development with Idris for an example of encoding critical information into the type system. Beyond that, see SPARK where you're limited to a provable subset of the Ada language (the subset has been extended with each version) so you can make assertions and it will attempt to prove (as part of compilation) that the assertio…

Combine Spark with Z as a specification language and you can get to "correct by construction". The only problem seems to be a reluctance to actually formulate a spec.

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

#59

Post by jpollock »

tpmx wrote: post #2

This didn't age very well. Especially the part celebrating "over-engineering" including the explicit duplication of code, instead of re-use, since that is "risky". I do however like the strong emphasis on (manual) testing.

Code reuse can result in failures. Sometimes those failures are big and loud. The Ariane 5 failure also happened in 1996, which is quite funny. :)

https://www.bugsnag.com/blog/bug-day-ariane-5-disaster

https://www.youtube.com/watch?v=gp_D8r-2hwk

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

#60

Post by xmprt »

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.
Post reply on HN