91–100 of 126 posts
Are there any research projects trying to make "proof" programs / languages?
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…
Formal verification is huge these days I would like to think.
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...
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.
Few algorithms are as battle-tested as the sorting algorithm from the Java standard library. I can't even estimate how many calls are made to this function every day. The fact that we can still find bugs in it, no matter how obscure, suggests to me that we simply can't write correct nontrivial software without proof.
The victory isn't in showing that this specific algorithm is incorrect in some fairly obscure way. It's in the fact that even software that's this battle-tested is still not fully reliable.
Earlier quoted context omitted.
The bolts don't, and yet they don't (usually) fail.
What do you mean? They're designed and tested according to calculations done by mathematically proven methods.
Earlier quoted context omitted.
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.
Earlier quoted context omitted.
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…
5) Some software is formally verified Formal verification is huge these days I would like to think.
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.
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...
The main advantage of open source for me isn't that all bugs are found. It's that when I encounter a bug I can check the code, report it, fix it in my fork and get it fixed in the main repo eventually.
With closed source you have to make do with workarounds.
Earlier quoted context omitted.
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…
5) Some software is formally verified Formal verification is huge these days I would like to think.