tl;dr: The testing of code is done by intelligent adversaries.
That's a poor TL;DR for this paper. It contains a lot more than that.
How Did Software Get So Reliable Without Proof? (1996) [pdf]
21–30 of 126 posts
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#22One 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.
I don't think that's true, or at the very least it's misleading. Qualified eyeballs are often expensive, and moreover there are consistent intellectual biases of human beings that interfere with catching all bugs.
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.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#23One 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.
I don't think that's true, or at the very least it's misleading. Qualified eyeballs are often expensive, and moreover there are consistent intellectual biases of human beings that interfere with catching all bugs.
Though the 'law' is associated with reading source code, I think it can also apply to people using the code, and reporting errors (sometimes automatically).
They may not be able to fix it, but just noticing there is a problem is a big first step.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#24A relevant paper to discuss alongside this one: https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf
Social Processes and Proofs of Theorems and Programs
Even rigorous mathematics requires social processes to become 'reliable', ie truthful.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#25Are there any research projects trying to make "proof" programs / languages?
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#26Earlier quoted context omitted.
I don't think that's true, or at the very least it's misleading. Qualified eyeballs are often expensive, and moreover there are consistent intellectual biases of human beings that interfere with catching all bugs.
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.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#27It 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.
It is also replacing humans most of the time as well, who are prone to making all sorts of errors. Worse, humans can make the same error twice even after being corrected.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#28The first sentence of the article begins "Twenty years ago", and yet the article itself is undated. This appears to be entirely normal for scientific papers. Can anyone tell me how this foolishness came to be considered acceptable among scientists, and why it persists?
It depends on how you come across the paper. Peer-reviewed scientific journals (as well as some preprint channels that aren't peer reviewed) are fully explicit about the date of publication. However, if those same papers are published on another website, they might lack metadata such as date and publication venue. This is a good reason to link to the actual publication source instead of to a PDF copy of the paper (un…
> 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.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#29Are there any research projects trying to make "proof" programs / languages?
Yes, this is an extremely active area of research with lots of connections in the broader programming languages and formal methods communities. For the last decade or so, POPL has had a co-located workshop on proof, the programs of which would be a great place to see the current state of the art. Here's last year's: https://popl20.sigplan.org/home/CPP-2020#event-overview
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#30user find bug, dev fix bug. happy path!
other path: dragons be here
The tree or tributary structure of software suggests that deeper, more fundamental, more general bugs will be revealed first and frequently. And logically will be fixed at the root, rather than hacking at the myriad leaves... right...?