How Did Software Get So Reliable Without Proof? (1996) [pdf] • Hacker News Board

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

#11

Post by londons_explore » Thu, Sep 17, 2020, 9:07 PM UTC

javiramos wrote: post #5

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.

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

In most other fields, there are far fewer eyeballs, because far less work is opensource.

If most/all CAD designs were opensource, you can imagine there would be projects underway to automatically "find all screws in the world that are too short to hold the design load". With enough projects of that nature, standards across the entire field will improve.

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

#12

Post by tsorferaoh » Thu, Sep 17, 2020, 9:07 PM UTC

mjw1007 wrote: post #6

The 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?

Presumambly the PDF doesn't include the date because it is camera-ready copy for a journal (in this case the filename includes the year of publication).

In general, I'd say people are sloppy about this because publishing is like a super-public form of notarization, which has the effect of placing the name of the article into public indices and databases, most importantly the list of contents of that journal. It's not that people don't care about the date—it's that they have no difficulty finding out what it was.

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

#13

Post by CobrastanJorji » Thu, Sep 17, 2020, 9:10 PM UTC

mjw1007 wrote: post #6

The 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?

I presume it's a slow feedback loop. It's always fine immediately after you do it, and I don't think brains learn very well from small mistakes we made years ago.

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

#14

Post by wukkuwukku » Thu, Sep 17, 2020, 9:12 PM UTC

mjw1007 wrote: post #6

The 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?

https://www.gwern.net/docs/math/1996-hoare.pdf

1996 is in the URL.

This is less a science thing and more an Internet culture thing, IMO.

Documentation norms online have changed with variablized URLs full of computed data

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

#15

Post by hcarvalhoalves » Thu, Sep 17, 2020, 9:12 PM UTC

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.

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

#16

Post by mjw1007 » Thu, Sep 17, 2020, 9:12 PM UTC

londons_explore wrote: post #7

mjw1007 wrote: post #6

The 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?

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 date at all.

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

#17

Post by mjw1007 » Thu, Sep 17, 2020, 9:17 PM UTC

tsorferaoh wrote: post #12

mjw1007 wrote: post #6

The 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?

Presumambly the PDF doesn't include the date because it is camera-ready copy for a journal (in this case the filename includes the year of publication). In general, I'd say people are sloppy about this because publishing is like a super-public form of notarization, which has the effect of placing the name of the article into public indices and databases, most importantly the list of contents of that journal. It's not…

I observe that the same is true for the paper's authorship information, but nobody seems to have any difficulty placing that prominently near the top of the document itself.

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

#18

Post by thaumasiotes » Thu, Sep 17, 2020, 9:17 PM UTC

mjw1007 wrote: post #16

londons_explore wrote: post #7

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…

> 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")

Doesn't matter. If the author was thinking of a specific year, they'd say the year. If they say "20 years ago", everything that was "20 years ago" this year is also "20 years ago" a couple years from now.

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

#19

Post by mjw1007 » Thu, Sep 17, 2020, 9:20 PM UTC

thaumasiotes wrote: post #18

mjw1007 wrote: post #16

Earlier quoted context omitted.

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…

> 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") Doesn't matter. If the author was thinking of a specific year, they'd say the year. If they say "20 years ago", everything that was "20 years ago" this year is also "20 years ago" a couple years from now.

It's common for papers to include words like "recently", or indeed "has not yet", which are rather more time-sensitive and still don't specify an exact year.

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

#20

Post by Jtsummers » Thu, Sep 17, 2020, 9:20 PM UTC

From the conclusion:

> Formal methods researchers who are really keen on rigorous checking and proof should identify and concentrate on the most critical areas of a large software system, for example, synchronisation and mutual exclusion protocols, dynamic resource allocation, and reconfiguration strategies for recovery from partial system failure. It is known that these are areas where obscure time-dependent errors, deadlocks and livelocks (thrashing) can lurk untestable for many years, and then trigger a failure costing many millions. It is possible that proof methods and model checking are now sufficiently advanced that a good formal methodologist could occasionally detect such obscure latent errors before they occur in practice. Publication of such an achievement would be a major milestone in the acceptance of formal methods in solving the most critical problems of software reliability.

I feel like this presages the way TLA+ (in particular) has had a relative surge among practitioners.