71–80 of 126 posts
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.
Programs or algorithms only guarantee that they can go from one state to another state.
Somehow computer programs have been conflated with relability and proof possibly because of close adjacency to mathematics.
If you account for survivorship bias, I would bet that software is not very reliable.
Proof is how the authors of this paper discovered that OpenJDK's java.utils.Collection.sort() was broken http://envisage-project.eu/wp-content/uploads/2015/02/sortin...
In my opinion its just not practical for most programmers to understand a book like "The science of programming" and consciously apply proofs each time they write code. Most programs can be delivered with bugs, These can be discovered and corrected over time. So having strong QA teams as an alternative to proofs should be the reason of having and abundance of reliable software.
Are there any research projects trying to make "proof" programs / languages?
> The seL4® Microkernel. Security is no excuse for bad performance. The benchmark for performance. The world's most highly assured OS kernel. Open source & community-supported under the seL4 Foundation.
Earlier quoted context omitted.
Because traditionally, articles were published in journals, and journals had the date written on the cover, so it was superfluous to add it on every page.
That seems rather sloppy to start with: you could easily end up a year or two out (the date that matters isn't the date of publication, it's the date that was in the author's head when they wrote something like "Twenty years ago"). In any case nowadays I think there's no excuse for this practice continuing. It's far too common for a paper to get sent around, or put on the author's personal website, with no associated…
Natural Selection. If you account for survivorship bias, I would bet that software is not very reliable.
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.
The level he works at might be higher level though. It sounds like control systems for airplanes are fairly modular.