11 ms·

How did software get so reliable without proof?

185 points by azhenley 7y ago

tboyd47 7y ago
Brilliant analysis.
temac 7y ago
Except that we continue to slowly automate away human intervention (must be done reasonably; it must still be possible, it is just less current in practice). Just look at the state of the art in field X at date T, then 10 or 20 years after. We are getting better at some software, and why would we not? Not all SW, but some, and even probably a lot of. Likewise for VLSI (which in some aspects is quite similar to SW); there are some quirks, but it basically works despite the modern designs being of unprecedented complexity. With a reliability way higher that tons of high ends mechanical devices. Same story for off the shelf standard operating systems even for absolutely not critical software: given the application are somehow tolerant to crashes (the user just restart), it is remarkable that we get so few. I'm a firm believer that there is no SW crisis. There are people or companies refusing to apply best practices here and there, or even not knowing they exist, but that is another story.
ssivark 7y ago
> How did software get so reliable without proof? Simple, software started shipping with more bugs in backlogs :-P — More seriously, software today is endemically crappy, and often poorly designed. I dunno why Hoare thought it was any better. The only saving grace is that (modern) software largely stays away from serious stuff. Eg: The airline industry is reluctant to upgrade software from decades ago, but happy to incrementally upgrade other pieces of the system on shorter cycles. Then of course, we have systems like the Boeing 737Max MCAS where the software did what it was supposed to (taken literally) but the software system was poorly designed. EDIT: Just remembered this fantastic talk by Joe Armstrong https://youtu.be/lKXe3HUG2l4 https://youtu.be/lKXe3HUG2l4 The smooth running of every abstract system depends crucially on the (human) operator handling the point of contact with reality, in practice, often bending reality to make it tractable for the system. Any bureaucracy would grind to a halt if it wasn’t intelligent humans carrying out the processes! Software is no different. Just like it’s hard to take a technology from “zero to one”, it is hard to take the amount of necessary human oversight from one to zero. For this reason, I would much rather think of software as amplifying the capabilities of that human, rather than automating away other humans. In practice, these systems will end up needing a highly skilled and trustworthy human operator to shepherd them — might as well design the system to make it maximally easy for those operators to understand/debug/tweak.
- WalterBright 7y ago
  > software today is endemically crappy, and often poorly designed So is every other engineering product that hasn't gone through years (decades) of evolutionary refinement.
  - averros 7y ago
    Not really. When programming was done by real engineers (rather than "coders", "developers", or horribly misnamed "software engineers") - with proper engineering discipline which involved deliberate design and documentation rather than "agile" hacking, it was more reliable. By far. My personal recent experience of actually doing software the old-fashioned way involved writing correctness critical high-performance code for a major data warehouse vendor, which mostly stayed with zero known bugs in production - greatly contributing to the vendor's reputation as reliable and dependable place to keep your data in. And how do I know what the old-fashioned way to write code is? Well, I've been writing code professionally for nearly 40 years.
    - ColanR 7y ago
      The more I learn about modern software practices, the more I come to think that software is worse today because programmers are poorly disciplined and badly trained. Of course, that's likely because the barrier to entry is so much lower today than it used to be.
      - WalterBright 7y ago
        The barrier of entry to software has been zero ever since the 8080 was introduced.
        fxtentacle 7y ago
        Back then there were a lot less stackoverflow copy & paste mistakes.
diroussel 7y ago
So I guess the answer is: because of the feedback loops that exist around the software systems.
- perrygeo 7y ago
  Exactly. Software systems are reliable because they have economic value. We're incentivized to make them work, regardless of how much technical debt and duct tape lies under the hood.
tschmidleithner 7y ago
> The ultimate and very necessary defence of a real time system against arbitrary hardware error or operator error is the organisation of a rapid procedure for restarting the entire system. "Just putting out the plug and stick it back in" is one common way nowadays of how to get out of an unforeseen state. It has quite some history and goes at least back to the "let it crash" philosophy of Erlang. Of course this still does not work for all kind of domains, especially when one is closer to the metal. But still, we may have found a sufficiency compromise between formal verified software (and thus, higher costs) and some kind of fault-tolerant software (increased productivity).
- beetwenty 7y ago
  Or, in another word, "disposability". We have a lot of systems that aren't repairable, don't get debugged, don't have things fixed mid-flight. And...it works, with respect to most existing challenges. Restarting and replacing is easy to scale up and produces clear interface boundaries. One way in which it doesn't work, and which we still fail, is security. Security doesn't appear in most systems as a legible crash or a data loss or corruption, but as an intangible loss of trust, loss of identity, of privacy, of service quality. We don't know who ultimately uses the data we create, and the business response generally is, "why should you care?" The premise of so many of them, ever since we became highly connected, is to find profitable ways of ignoring and taking risks with security and to foster platforms that unilaterally determine one's identity and privileges, ensuring them a position as ultimate gatekeepers.
- triangleman 7y ago
  I'm already starting to get tired of all these frequently-restarting Nomad jobs, and I've only been at it for a few months.
m463 7y ago
As a software person, I found Richard Feynman's paper "Personal Observations on Reliability of Shuttle" quite interesting. https://www.history.nasa.gov/rogersrep/v2appf.htm https://www.history.nasa.gov/rogersrep/v2appf.htm The part about software reliability stuck in my head, because he quickly came to the conclusion it was fine. Now shuttle software is probably the most special type of software on the planet, but it made me think how reliable software is... compared to hardware (and possibly people).
- perl4ever 7y ago
  Physical things tend to not yield to abstractions as much. While people talk about how difficult software debugging is when the illusion of a high level abstraction is broken, still it's more of an exception.
stared 7y ago
Isn't it evolution and Darwinian selection? Bad pieces tend to die out, good pieces get replicated, "breed", mutated and incorporated[1]. Biological systems are not fault-tolerant. They are resilient on the average, under typical conditions. [1] Among species, we get vertical transfer of genes (parent(s) to offsprings), horizontal (e.g. plasmids between bacteria). Getting as a piece of DNA as a submodule (this element-of relationship) is rare... but happens (e.g the mitochondrium). In software, it is one of the most common relationships.
- JoeAltmaier 7y ago
  Not quite? Life is resilient under the worst case. If it weren't, the first time the worst case came around (drought year/early freeze/whatever) that form would become extinct. Sure there's a distribution (gene pool) and some is merely resistant under normal conditions. That kind prospers, but keeps the 'worst case' genes handy. A few members of the population are the 'prepper' members, and if this year is the worst case then the species survives. Anyway something like that.
  - stared 7y ago
    Drought is still a "typical" condition. (I.e. one from its environment, from the last hundreds of thousands of years or so.) Selection pressure worked on that. Yes, it may be a condition that makes 10%, 50% or 90% percent of the population to die - and it is not a problem, in the grand scheme of things. Not normal conditions are things that were never tested, or never tested to that extend. E.g. an invasive species from a different continent, a chemical compound, different pH of water, etc. Consequently, many species die out completely - as there is not enough time for the selection of better-fitted genes for this setting. Also: compare with machine learning, and giving a sample out of the training dataset distribution (all photos are shot in good light, give one in the dark). Usually, the answer is meaningless.
- TheOtherHobbes 7y ago
  Selection depends on a fitness function. The fitness function for a lot of software is some weighted combination of profitability, mindshare, and novelty, not some abstract measure of quality and stability.
wanderr 7y ago
Human operators surely play a part sometimes, but there are systems which eliminate or minimize that and are still surprisingly reliable. I think people have learned to build resilience into their systems, which expect and anticipate failures. These systems still fail and when they do it's often in very complex and surprising ways, but those failures are rare.
- abraxas 7y ago
  Interesting. I wonder if there is a point beyond which multiplying these abstractions doesn't really do anything to boost either performance or reliability i.e. will someone come up with a way to wrap and package kubernetes clusters into yet another russian doll abstraction?
  - wanderr 7y ago
    I actually wasn't thinking in terms of abstractions although those can help too. Simple things like always validating your inputs, adding sanity checks and safety limits to your code, building in isolation, can go a long way towards catching a lot of errors and/or limiting the blast radius of failures.
sitkack 7y ago
By begging the question!
agentultra 7y ago
Maybe it has something to do with most software not only being not right but not being wrong either (I’m paraphrasing Wolfgang Paul). We do put a lot of effort into writing correct programs for some definition of correct. But a lot of our specifications don’t include things that aren’t obviously wrong like, “not leaking secrets,” wrong. I share the enthusiasm of SPJ who said, “it’s amazing that it works at all let alone so well.” It’s easy to forget that that little white box you type a few words into is more impressive in scope and complexity than the tallest buildings humans have built. And yet it is so largely invisible! I think the more important question is how much longer have we got left before regulators and insurers demand we assume more liability for things when they do go wrong.
- gonzo41 7y ago
  I actually think that the FOSS movement and licensing is really progressive in this space. This thing comes with NO Warranty etc is really great because you own the risk of the systems you build. If only that got surfaced more to the users so they realized that a T&C page isn't really protection for anything. Rather than force devs to use formal methods, I'd really like it if software got to the point where regulators and insurers demand that we treat personal information like radioactive waste and try and handle the least amount possible.
  - agentultra 7y ago
    > Rather than force devs to use formal methods I don't think professional liability would require all developers to use formal methods any more than it would require all practicing software developers to become licensed engineers. It may require companies to hire a licensed engineer to sign off on projects and it could require those engineers to be insured so they may want to use formal methods on a risky project to keep their rates down. The end result, I think, is the same: pressure to do better by the standards of the state of the art and not skimp on privacy and security.
dekhn 7y ago
I've worked on software for some time and have seen a wide range of interesting failure modes. All of the interesting failures (some of which have had large monetary or visible outage impact) involved systems that broke in ways that aren't well-addressed by proof systems. Instead, they've been about things like statistical binning of parts, rare errors that escaped through middling checksums, and complex distributed systems. In most of these cases, there is some physical component, such as corrupted packets which pass CRC checksum, or a chip that occasionally miscomputes the hash of a string. Not sure how proof systems handle this, but in practice, those have been some of the most impactful errors, and they are typically dealt with using heavy but not comprehensive software testing.
- lmm 7y ago
  In my experience the interesting failures are a tiny fraction of the failures; your mind just glosses over the vast sea of boring failures. The most impactful software flaws have not been subtle logic misalignments, they've been utterly basic errors like Cloudbleed or the Arianne 5 overflow. Maybe proof systems can only address 99% of software failures; my guess is that with experience we'll find ways to cover the rarer cases as well, but even if we don't, they're still worth using.
  - jwhitlark 7y ago
    Well, maybe. Additional costs with these approaches are often ignored. I wouldn't want to give up proof systems as a tool, but too many treat them as a zero cost panacea. A proof system or type checker is not an excuse to not give a fk about your craft, but I've seen it that way more frequently than I'd like to admit. Personally and honestly, outside of already well understood or defined systems, I'd say that people should invest their time in understanding their business domain, before they dig deep into proofs and related techniques.
    - lmm 7y ago
      > Well, maybe. Additional costs with these approaches are often ignored. I wouldn't want to give up proof systems as a tool, but too many treat them as a zero cost panacea. A proof system or type checker is not an excuse to not give a fk about your craft, but I've seen it that way more frequently than I'd like to admit. The acceptable defect rate to the business is presumably fixed, so if a proof system or type system reduces you defect rate below that then that should be an "excuse" to write fewer tests and move faster, as icky as it feels to do that. I find the maintenance burden of tests is often underestimated; types in particular may not be free, but they get you more bang for your buck than any alternative, in my experience. > Personally and honestly, outside of already well understood or defined systems, I'd say that people should invest their time in understanding their business domain, before they dig deep into proofs and related techniques. Isn't it the same thing though? Encoding your business domain into the system you're using is the hardest part of using any formal system, but it's also an excellent way of forcing you to really understand the domain.
wisnesky 7y ago
In 2020, software is reliable?
pshc 7y ago
Simply an absurd amount of hard work. Millions upon millions of person-hours spent banging foreheads against C++ and the like. Billions of gray hairs. But that’s progress for you.
super_trooper 7y ago
Probably money? If there is money to be made somebody is going to find a solution that mostly works
zwieback 7y ago
By focusing on the critical path through the call tree. It's shocking how many fatal errors static analysis finds in my typical C/C++/C# code but the call graph that those errors are on simply never gets exercised. The mathematical proof would include all those unused paths.
dimes 7y ago
The proof is in the pudding.
jerf 7y ago
Every piece of software defines an input space of all possible inputs for that software. This space is staggeringly, exponentially enormous. However, the space of inputs that are actually given to the software are generally an exponentially small subset of the possible inputs. Making this often very stereotypical and "friendly" space of inputs do mostly sensible things is at least polynomially, if not exponentially, simpler than making the software be entirely correct. It is both true that software is a streaming pile of bugs, where the vast, vast majority of responses to possible inputs is somehow wrong, yet the vast, vast majority of inputs actually processed by the software are mostly correct (not entirely, but mostly) because they are in the generally polynomial subsets of the exponentially complicated space that the developers made correct... ish.
- sansnomme 7y ago
  To expand on this, floating point works for 95% of programs. It is the 5% that needs exact accuracy/precision offered by arbitrary precision libraries. Most programs hardly exhaust the entire range of your typical floating point usage range. For example in a GUI you won't be able to easily tell the difference between 100% and 99.9999999% by eyeballing.
- vonseel 7y ago
  I think I’ll use your comments as a response next time someone calls me out in a code review or says I deployed a bug. Specifically the polynomial exponentially complicated bits. The look on their faces would be priceless. And they would forever think I’m a jerk... since they wouldn’t get the sarcasm lol.
- hcs 7y ago
  This is why model checking and directed fuzzing are so effective! There are situations so stupid only a machine, or reality, could come up with them.
wyager 7y ago
> How did software get so reliable Talk about begging the question!
- pjscott 7y ago
  How many HTTP request does nginx usually serve before crashing? How long can a Linux kernel stay up before panicking? Some complex software is startlingly reliable.
AnimalMuppet 7y ago
1. Proof costs. Like, a lot. If you don't need the reliability, why would you pay for it? 2. How much reliability is needed? Not 100% (usually). If my OS crashes, I'm unhappy. If the OS on my company's production server crashes, that's a lot worse. But our production server is actually a redundant cluster, so if one machine crashes, people are unhappy, but nothing horrible happens. (In point 1, I talked about the cost of proven-to-be-perfect software. Needing to have a redundant cluster is part of the cost of not having perfect software, which also must be considered. But because the hardware isn't 100% reliable either, we needed a redundant cluster anyway...) 3. Formal methods are often playing catch-up. Now we have to worry about timing side-channel attacks through the cache. There may now be formal methods to prove that such things are not possible in a piece of software; I'm pretty sure there were not such formal methods five years ago. We keep finding new areas that can fail. (One advocate of formal methods replied to me some weeks ago that formal methods proved that the software would never do anything that it wasn't specified to do. I doubt that claim with respect to something like side-channel attacks. Even if it's true, though, I suspect that often the specification didn't include "no side channel attacks" until certain recent events brought it to more popular attention.) Proofs are therefore suffering from a double whammy: Not only are they painfully difficult and expensive, but they're incomplete. When something comes up that wasn't covered by the proof of correctness, you now need to fix it. And then you have to re-run all the proofs all over again, because your fix may have invalidated them. 4. All proofs have to start somewhere, usually with a formal specification. If the specification is wrong (looking at you, MCAS), all the formal proofs in the world won't save you. (Well... a system-level formal proof might. But that's even harder and more expensive. And even that fails if the system spec is flawed.) TL;DR: Real proofs are too expensive for the benefit they provide, in almost all cases. The cost-benefit just isn't there. Hope lies in making them easier and more automated to use (better type systems, for example).
panic 7y ago
How did proof itself get so reliable? The process of convincing yourself that a proof is correct isn't so different from the process of convincing yourself that a program is correct.
- hcs 7y ago
  And equivalently, if you had heavily-relied-on proofs that were as narrowly read and hard to follow as software, mathematics would be in just as bad a state.
- garmaine 7y ago
  Yes, it is. This can be shown with theory: proving a program is correct is NP-hard, but verifying the proof is in P-space. It is way easier to show a proof is correct than to generate the proof in the first place.
  - panic 7y ago
    True, at least for formal proofs. I was thinking more of traditional mathematical proofs, which are often as hard to formalize as programs are to prove correct. In both cases, convincing yourself that the proof or program is correct involves reading it and seeing whether each of its parts follows from or fits into the other parts to make a coherent whole. Of course, there are ways to fool the reader, but I think people learn to avoid writing in ways that are likely to mask errors (e.g., not reusing the same symbol to mean completely different things, both in proofs and in programs).
gandalfgeek 7y ago
Short explainer video covering Hoare's original paper: https://youtu.be/eY8AyCZ5uUg https://youtu.be/eY8AyCZ5uUg
hcarvalhoalves 7y ago
The most trivial software system you can think of nowadays is already so large in scope and/or complex that you can’t prove it doesn’t work either, because there’s no complete specification on how it’s supposed to work - if it existed, it would be the bug-free software itself, because all software is specification. In the end all that matters is whether the system is useful, in an economical sense (value delivered > defects over time). So I would argue software did not get reliable, our bar for defects remained low, but the relative value delivered increased a lot because software has amazing leverage.
- hcs 7y ago
  Moreover, when you get an existence proof of a bug, it's usually easy to change such a system to seem ok. As Hoare also said, "There are two methods in software design. One is to make the program so simple, there are obviously no errors. The other is to make it so complicated, there are no obvious errors."
_bxg1 7y ago
Fascinating how perception has changed since then; I think most people today would have the opposite sentiment: "How did software get so unreliable?" My guess is: software creation and distribution became exponentially more accessible around that time (1996) with the advent of the web. Not only were many less-qualified individuals creating software (which isn't intrinsically a bad thing!), many more people were consuming software (making consumer software a much more lucrative market), and technology changes allowed companies to "move [much] fast[er] and break [more] things". Businesses were always optimizing for profits, and the dot com boom simply changed the equation to where reliability was no longer profitable in the majority of the field.
gelo 7y ago
Most of the software I have written for work has no near on no functional / unit tests. It is industrial process monitoring software that runs 247 on remote machines thousands of miles away. Simple fact is it has to work, no if's but's, even when there are faults in its environment. This does not mean to say that the software has not been tested. Testing is subjective to a softwares use. You could have 10000 tests and still have a series of bugs. Testing for my work comes as two categories, "Tested by design" and "Environmental Testing". "Tested by design" involves developing your software by which the designing and writing the software inherits the tests as you go. When I go about designing a feature, I expand on a chosen solution of that feature and then methodically branch out on the uses of that feature, build a map of dependancies, scenarios, outcomes, consequences etc for that feature. These become the basis of how I write the code for that feature because I have inherantly put in mitigations for everything I have considered before hand. There is no point in testing something excessively if you can and/or have garanteed by code that it will perform exactly as designed. That may seam a contraversial thing to say. With "Environmental Testing" we simulate the environment which the software is put into with real external factors. This is particular for the software I write. This is not always the best for another software project. I've written my works software from scratch 3 years ago and it has had various incremental additions and changes. Yes there have been bugs. I will admit that entirely. However the key thing with work's software is that is has rarely crashed or rarely faulted while containing those bugs. Most faults that have been found have been configuration errors/issues. I would be interested in how others approach testing strategies for the software they have written.
pjscott 7y ago
How does software get reliable at all, ever? In my experience there are two ways: 1. You write reliable software from the start. It feels a lot like writing a mathematical proof, or at least sketching one. After a few dumb bugs are fixed the code continues to work without issue, year after year, and nobody ever looks at it again. (This isn't as hard as it sounds! It's not the right approach for everything, but it should be more widely used than it is.) 2. You write normal software, i.e. unreliable crap, but you look at the ways that it goes wrong and fix them. This requires that you put some work into detecting that things have gone wrong. A lot of software companies will trace all crashes, and aggregate stack traces and logs from them. In this kind of environment, you can improve software reliability by sticking a paranoid number of assertions in your code and obsessively checking to see what triggered them. After a while all the common problems will have been removed, and the remaining bugs will be less prevalent than hardware failures -- and then you can declare victory.
- pif 7y ago
  From my experience, the problem with no. 1 is that, in order to build something correct, you have to know what you need to build, and that is a can of worms (actually, a snakes nest) that too many people refuse to address. The problem with no. 2, on the other side, is that it will eventually get correct, but you cannot predict when it will be reliable. And the same people who refuse to sign requirement documents are the same people who insist on having arbitrary deadlines.
  - rstuart4133 7y ago
    > The problem with no. 2, on the other side, is that it will eventually get correct Actually, it doesn't necessarily get correct. There are old programs out where the ratio of bugs fixed by a modification / bugs introduced is less than 1. For small systems this never becomes a problem, but huge complex systems it really is a thing. The only way I know of to prevent it from happening is unit tests with excellent coverage and CI.
- moksly 7y ago
  In my experience the majority of enterprise service applications and smaller few-purpose systems are build following 1. We’ve have an ASP Web Forms food ordering system that’s basically four forms and a simple CRUD admin system page that’s been running flawless for half a decade. It’s only needed upgrades to its .NET system as we moved up the TLS version ladder, and it has thousands of daily users. There are no tests, no real monitoring outside of “is it still up?” and no complaints. Eventually we’ll have to clean up the database, eventually. But chances are someone will have build something new by then.
kazinator 7y ago
> How did software get so reliable without proof? Two words: survivorship bias! The software field exploded in the past half a century, producing a huge volume of activity producing a huge amount of cruft. A lot of the unreliable stuff gets shaken out; so what we see is a biased sample consisting of the successes that remain. Software that is halfway successful gets to be maintained, and over many years or decades, the reliability improves.
buzzkillington 7y ago
The main reason I've found for programs being 'correct' is that the range of actual inputs for programs is severely limited. Most programs see inputs that are similar enough to previous inputs that the latent bugs are never triggered, or at worst triggered one at a time. Running programs far outside their expected parameters on the other hand has nearly always lead to disaster.
- amelius 7y ago
  Would you say that a typical web-browser (a complicated piece of software) always sees the same kind of input?
  - buzzkillington 7y ago
    Pretty much. Throwing [0] to chrome and firefox has made made them hang for 5 minutes so far. Generating the HTML took under a second and 13MB, large, but not larger than the fatter webpages out there. In terms of input browsers don't see but should be able to parse you can't get much simpler than this. [0] In Guile2.x: (define print (lambda (x) (display x) (newline))) (define div-hell (lambda (n) (cond ((eq? n 0) (print "TEXT")) (else (print "<div>") (div-hell (- n 1)) (print "</div>"))))) (print "<html><header><title>DIV HELL</title></header><body>") (div-hell 1000000) (print "</body></html>")
justlexi93 7y ago
The same way bridges, aeroplanes and medicine happened. What makes software so special?
tus88 7y ago
Fixed a ton of bugs. And it's not that reliable, and super reliable software in airplanes is proved.
aprdm 7y ago
Having worked in some places that aren't software companies it is pretty incredible how something a developer who is no longer in the company set in the last decade is still kicking ass with no monitoring or documentation. It's truly remarkable! All those databases that software depend on and go without people even realizing they exist until someone literally decomissions a datacenter only then to figure out lots of apps require that particular machine to be running... they're day in and day out working with 0 maintenance for years... impressive. Postgres, mysql and mongodb are examples of databases I've seen like that! As well as inhouse apps that depend on those databases... at most they have a cron job for backing up and keeping at most the last X backups.
speedplane 7y ago
This article misses the elephant in the room: how to define "reliability". Most software perceived to be reliable (eg, MS Paint, bash) have numerous bugs, it's just that no one comes across them. Software that is perceived to be "reliable enough" (eg, MS Word, Chrome), have bugs that pop up regularly. Here are some vague uptime reliability measures and what you need to get there: - 70% reliability: you can often just free-code it and pray. - 95% reliability: you better have a bunch of tests. - 99.5%: you need automated testing, coverage tools, documentation, team coordination tools, and and solid merge/deployment process. - 99.99%: all-of-the-above plus tests that aggressively attack and analyze production systems (eg, Netflix Chaos Monkey), coverage tests that do branch coverage and not just line coverage, simulating network failures, and/or test on a variety of hardware and user-configurations. - 100%: The only way to be absolutely certain, is to convert each line of code into a mathematical operator and solve for a formal proof of correctness. The 100% reliability standard is not just theoretical. The U.S. government issues software standards for safety critical devices (military, aviation, healthcare), and some of them do indeed require mathematical proof of correctness (EAL6+ being a key standard). They generally do not require 100% bug-free code, but just that some particular features are 100% bug free (e.g., the OS/scheduler will never deadlock).
- yaantc 7y ago
  > and some of them do indeed require mathematical proof of correctness > (EAL6+ being a key standard) Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS. [1] https://www.commoncriteriaportal.org/products/ https://www.commoncriteriaportal.org/products/
  - speedplane 7y ago
    > Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS. You are definitely correct. Also, disclosure... I worked on that EAL7 Virtual OS. When I left it was only EAL6+, likely leading to my bias towards it.
otabdeveloper4 7y ago
If you compare K&R C and C++17, everything that has been added is some form or another of 'proofs'. So I take issue with the 'without proof' part; even if they're not proofs that adhere to strict mathematical forms, they're still there.
LoSboccacc 7y ago
most software today is a mess. only when you include the user in the loop with his version-3-new-final backups and willingness/need to retry in the event of error you get something that's workable. we've effectively shifted partial blame on the users, the famous "operator error" class of bugs, made sure to help then save often and substituted reliability with resilience but it doesn't mean software is reliable. the whole system as a whole and including users corrective actions is somewhat resilient enough for productive work
lngnmn1 7y ago
Exactly the same way as life itself got so reliable - by trial and error and selection of what is stable. /thread
tzjmetron 7y ago
Software is as reliable as the world we live in - basically, unreliable. Does that matter though? Practically, no. If it works well enough, it's good enough.
cjfd 7y ago
By fixing everything that goes wrong noticeably and by having no idea that many features are currently actually not working as they are supposed to? To actually create reliable software currently the best bet is to have automated tests for as many things as possible and exploratory manual testing around any feature that changes.
hannob 7y ago
I think the answer to the question posed may just be "it's like natural selection". A lot of software is horrifically bad. But not all flaws are created equal. A software that runs an online shop, but crashes 50% of the time during checkout will probably not create a successful company and thus won't survive long. However a software that has comparably many flaws and fails in all kinds of rare corner cases, but still gets the job done in most average cases, may just survive, even though it's equally bad.
p0nce 7y ago
How did people get the impression software was so reliable?
crimsonalucard 7y ago
>The problem with the question “How did software get so reliable without proof?” is that it’s asking the wrong question. It’s not that software got so reliable without proof: it’s that systems that include software got so reliable without proof. No. This person isn't sounding smart enough. The real question isn't how systems that include software got reliable without proof but instead the reverse: how did software that includes systems get so reliable without proof? That's how you should conclude an article with some hand wavy technical jargon.
amelius 7y ago
> How did software get so reliable without proof? Because most software is just moving data from one place to another, combined with some very simple business logic.
qubex 7y ago
What strikes me in both the original article and the post is the failure to recognise that a strong form of selective pressure is being applied upon software, and that adaptive processes (of which evolution is but a single example) tend to optimise for the criterion that is being selected for even in absence of an overarching design (‘proof’). I recommend reading Darwin Among the Machines for comparison to hardware.
jacquesm 7y ago
I don't think software is all that reliable. Almost every piece of major software that I use has one or more bugs and periodically locks up or crashes. We as users have been conditioned to accept this with the situation getting worse rather than better over the years. The main reason software seems more reliable than in the past is because in a SaaS environment the crash doesn't happen on your computer anymore. But the effect is the same unless extreme care was taken on the server side to ensure that no data was lost. In most cases we perform the equivalent of a reboot or retry: we reload the page.
shekharshan 7y ago
When it comes to writing reliable software the best paper I have read is “Design By Contract”. That one paper combined with proper usage of exceptions will go a long way in preventing bugs. Of course there is also a need for more rigor in requirements.
rkagerer 7y ago
It didn't.
egberts1 7y ago
Richard Feynman said it best: 1. Write down the problem 2. Think real hard 3. Write down the solution http://wiki.c2.com/?FeynmanAlgorithm http://wiki.c2.com/?FeynmanAlgorithm
waynesonfire 7y ago
See Betteridge's law of headlines.

185 points by azhenley 7y ago

Brilliant analysis.

Except that we continue to slowly automate away human intervention (must be done reasonably; it must still be possible, it is just less current in practice). Just look at the state of the art in field X at date T, then 10 or 20 years after. We are getting better at some software, and why would we not? Not all SW, but some, and even probably a lot of. Likewise for VLSI (which in some aspects is quite similar to SW); there are some quirks, but it basically works despite the modern designs being of unprecedented complexity. With a reliability way higher that tons of high ends mechanical devices. Same story for off the shelf standard operating systems even for absolutely not critical software: given the application are somehow tolerant to crashes (the user just restart), it is remarkable that we get so few. I'm a firm believer that there is no SW crisis. There are people or companies refusing to apply best practices here and there, or even not knowing they exist, but that is another story.

ssivark 7y ago

> How did software get so reliable without proof? Simple, software started shipping with more bugs in backlogs :-P — More seriously, software today is endemically crappy, and often poorly designed. I dunno why Hoare thought it was any better. The only saving grace is that (modern) software largely stays away from serious stuff. Eg: The airline industry is reluctant to upgrade software from decades ago, but happy to incrementally upgrade other pieces of the system on shorter cycles. Then of course, we have systems like the Boeing 737Max MCAS where the software did what it was supposed to (taken literally) but the software system was poorly designed. EDIT: Just remembered this fantastic talk by Joe Armstrong https://youtu.be/lKXe3HUG2l4 https://youtu.be/lKXe3HUG2l4 The smooth running of every abstract system depends crucially on the (human) operator handling the point of contact with reality, in practice, often bending reality to make it tractable for the system. Any bureaucracy would grind to a halt if it wasn’t intelligent humans carrying out the processes! Software is no different. Just like it’s hard to take a technology from “zero to one”, it is hard to take the amount of necessary human oversight from one to zero. For this reason, I would much rather think of software as amplifying the capabilities of that human, rather than automating away other humans. In practice, these systems will end up needing a highly skilled and trustworthy human operator to shepherd them — might as well design the system to make it maximally easy for those operators to understand/debug/tweak.

WalterBright 7y ago
> software today is endemically crappy, and often poorly designed So is every other engineering product that hasn't gone through years (decades) of evolutionary refinement.
- averros 7y ago
  Not really. When programming was done by real engineers (rather than "coders", "developers", or horribly misnamed "software engineers") - with proper engineering discipline which involved deliberate design and documentation rather than "agile" hacking, it was more reliable. By far. My personal recent experience of actually doing software the old-fashioned way involved writing correctness critical high-performance code for a major data warehouse vendor, which mostly stayed with zero known bugs in production - greatly contributing to the vendor's reputation as reliable and dependable place to keep your data in. And how do I know what the old-fashioned way to write code is? Well, I've been writing code professionally for nearly 40 years.
  - ColanR 7y ago
    The more I learn about modern software practices, the more I come to think that software is worse today because programmers are poorly disciplined and badly trained. Of course, that's likely because the barrier to entry is so much lower today than it used to be.
    - WalterBright 7y ago
      The barrier of entry to software has been zero ever since the 8080 was introduced.
      - fxtentacle 7y ago
        Back then there were a lot less stackoverflow copy & paste mistakes.

diroussel 7y ago

So I guess the answer is: because of the feedback loops that exist around the software systems.

perrygeo 7y ago
Exactly. Software systems are reliable because they have economic value. We're incentivized to make them work, regardless of how much technical debt and duct tape lies under the hood.

tschmidleithner 7y ago

> The ultimate and very necessary defence of a real time system against arbitrary hardware error or operator error is the organisation of a rapid procedure for restarting the entire system. "Just putting out the plug and stick it back in" is one common way nowadays of how to get out of an unforeseen state. It has quite some history and goes at least back to the "let it crash" philosophy of Erlang. Of course this still does not work for all kind of domains, especially when one is closer to the metal. But still, we may have found a sufficiency compromise between formal verified software (and thus, higher costs) and some kind of fault-tolerant software (increased productivity).

beetwenty 7y ago
Or, in another word, "disposability". We have a lot of systems that aren't repairable, don't get debugged, don't have things fixed mid-flight. And...it works, with respect to most existing challenges. Restarting and replacing is easy to scale up and produces clear interface boundaries. One way in which it doesn't work, and which we still fail, is security. Security doesn't appear in most systems as a legible crash or a data loss or corruption, but as an intangible loss of trust, loss of identity, of privacy, of service quality. We don't know who ultimately uses the data we create, and the business response generally is, "why should you care?" The premise of so many of them, ever since we became highly connected, is to find profitable ways of ignoring and taking risks with security and to foster platforms that unilaterally determine one's identity and privileges, ensuring them a position as ultimate gatekeepers.
triangleman 7y ago
I'm already starting to get tired of all these frequently-restarting Nomad jobs, and I've only been at it for a few months.

m463 7y ago

As a software person, I found Richard Feynman's paper "Personal Observations on Reliability of Shuttle" quite interesting. https://www.history.nasa.gov/rogersrep/v2appf.htm https://www.history.nasa.gov/rogersrep/v2appf.htm The part about software reliability stuck in my head, because he quickly came to the conclusion it was fine. Now shuttle software is probably the most special type of software on the planet, but it made me think how reliable software is... compared to hardware (and possibly people).

perl4ever 7y ago
Physical things tend to not yield to abstractions as much. While people talk about how difficult software debugging is when the illusion of a high level abstraction is broken, still it's more of an exception.

stared 7y ago

Isn't it evolution and Darwinian selection? Bad pieces tend to die out, good pieces get replicated, "breed", mutated and incorporated[1]. Biological systems are not fault-tolerant. They are resilient on the average, under typical conditions. [1] Among species, we get vertical transfer of genes (parent(s) to offsprings), horizontal (e.g. plasmids between bacteria). Getting as a piece of DNA as a submodule (this element-of relationship) is rare... but happens (e.g the mitochondrium). In software, it is one of the most common relationships.

JoeAltmaier 7y ago
Not quite? Life is resilient under the worst case. If it weren't, the first time the worst case came around (drought year/early freeze/whatever) that form would become extinct. Sure there's a distribution (gene pool) and some is merely resistant under normal conditions. That kind prospers, but keeps the 'worst case' genes handy. A few members of the population are the 'prepper' members, and if this year is the worst case then the species survives. Anyway something like that.
- stared 7y ago
  Drought is still a "typical" condition. (I.e. one from its environment, from the last hundreds of thousands of years or so.) Selection pressure worked on that. Yes, it may be a condition that makes 10%, 50% or 90% percent of the population to die - and it is not a problem, in the grand scheme of things. Not normal conditions are things that were never tested, or never tested to that extend. E.g. an invasive species from a different continent, a chemical compound, different pH of water, etc. Consequently, many species die out completely - as there is not enough time for the selection of better-fitted genes for this setting. Also: compare with machine learning, and giving a sample out of the training dataset distribution (all photos are shot in good light, give one in the dark). Usually, the answer is meaningless.
TheOtherHobbes 7y ago
Selection depends on a fitness function. The fitness function for a lot of software is some weighted combination of profitability, mindshare, and novelty, not some abstract measure of quality and stability.

wanderr 7y ago

Human operators surely play a part sometimes, but there are systems which eliminate or minimize that and are still surprisingly reliable. I think people have learned to build resilience into their systems, which expect and anticipate failures. These systems still fail and when they do it's often in very complex and surprising ways, but those failures are rare.

abraxas 7y ago
Interesting. I wonder if there is a point beyond which multiplying these abstractions doesn't really do anything to boost either performance or reliability i.e. will someone come up with a way to wrap and package kubernetes clusters into yet another russian doll abstraction?
- wanderr 7y ago
  I actually wasn't thinking in terms of abstractions although those can help too. Simple things like always validating your inputs, adding sanity checks and safety limits to your code, building in isolation, can go a long way towards catching a lot of errors and/or limiting the blast radius of failures.

sitkack 7y ago

By begging the question!

agentultra 7y ago

Maybe it has something to do with most software not only being not right but not being wrong either (I’m paraphrasing Wolfgang Paul). We do put a lot of effort into writing correct programs for some definition of correct. But a lot of our specifications don’t include things that aren’t obviously wrong like, “not leaking secrets,” wrong. I share the enthusiasm of SPJ who said, “it’s amazing that it works at all let alone so well.” It’s easy to forget that that little white box you type a few words into is more impressive in scope and complexity than the tallest buildings humans have built. And yet it is so largely invisible! I think the more important question is how much longer have we got left before regulators and insurers demand we assume more liability for things when they do go wrong.

gonzo41 7y ago
I actually think that the FOSS movement and licensing is really progressive in this space. This thing comes with NO Warranty etc is really great because you own the risk of the systems you build. If only that got surfaced more to the users so they realized that a T&C page isn't really protection for anything. Rather than force devs to use formal methods, I'd really like it if software got to the point where regulators and insurers demand that we treat personal information like radioactive waste and try and handle the least amount possible.
- agentultra 7y ago
  > Rather than force devs to use formal methods I don't think professional liability would require all developers to use formal methods any more than it would require all practicing software developers to become licensed engineers. It may require companies to hire a licensed engineer to sign off on projects and it could require those engineers to be insured so they may want to use formal methods on a risky project to keep their rates down. The end result, I think, is the same: pressure to do better by the standards of the state of the art and not skimp on privacy and security.

dekhn 7y ago

I've worked on software for some time and have seen a wide range of interesting failure modes. All of the interesting failures (some of which have had large monetary or visible outage impact) involved systems that broke in ways that aren't well-addressed by proof systems. Instead, they've been about things like statistical binning of parts, rare errors that escaped through middling checksums, and complex distributed systems. In most of these cases, there is some physical component, such as corrupted packets which pass CRC checksum, or a chip that occasionally miscomputes the hash of a string. Not sure how proof systems handle this, but in practice, those have been some of the most impactful errors, and they are typically dealt with using heavy but not comprehensive software testing.

lmm 7y ago
In my experience the interesting failures are a tiny fraction of the failures; your mind just glosses over the vast sea of boring failures. The most impactful software flaws have not been subtle logic misalignments, they've been utterly basic errors like Cloudbleed or the Arianne 5 overflow. Maybe proof systems can only address 99% of software failures; my guess is that with experience we'll find ways to cover the rarer cases as well, but even if we don't, they're still worth using.
- jwhitlark 7y ago
  Well, maybe. Additional costs with these approaches are often ignored. I wouldn't want to give up proof systems as a tool, but too many treat them as a zero cost panacea. A proof system or type checker is not an excuse to not give a fk about your craft, but I've seen it that way more frequently than I'd like to admit. Personally and honestly, outside of already well understood or defined systems, I'd say that people should invest their time in understanding their business domain, before they dig deep into proofs and related techniques.
  - lmm 7y ago
    > Well, maybe. Additional costs with these approaches are often ignored. I wouldn't want to give up proof systems as a tool, but too many treat them as a zero cost panacea. A proof system or type checker is not an excuse to not give a fk about your craft, but I've seen it that way more frequently than I'd like to admit. The acceptable defect rate to the business is presumably fixed, so if a proof system or type system reduces you defect rate below that then that should be an "excuse" to write fewer tests and move faster, as icky as it feels to do that. I find the maintenance burden of tests is often underestimated; types in particular may not be free, but they get you more bang for your buck than any alternative, in my experience. > Personally and honestly, outside of already well understood or defined systems, I'd say that people should invest their time in understanding their business domain, before they dig deep into proofs and related techniques. Isn't it the same thing though? Encoding your business domain into the system you're using is the hardest part of using any formal system, but it's also an excellent way of forcing you to really understand the domain.

wisnesky 7y ago

In 2020, software is reliable?

pshc 7y ago

Simply an absurd amount of hard work. Millions upon millions of person-hours spent banging foreheads against C++ and the like. Billions of gray hairs. But that’s progress for you.

super_trooper 7y ago

Probably money? If there is money to be made somebody is going to find a solution that mostly works

zwieback 7y ago

By focusing on the critical path through the call tree. It's shocking how many fatal errors static analysis finds in my typical C/C++/C# code but the call graph that those errors are on simply never gets exercised. The mathematical proof would include all those unused paths.

dimes 7y ago

The proof is in the pudding.

jerf 7y ago

Every piece of software defines an input space of all possible inputs for that software. This space is staggeringly, exponentially enormous. However, the space of inputs that are actually given to the software are generally an exponentially small subset of the possible inputs. Making this often very stereotypical and "friendly" space of inputs do mostly sensible things is at least polynomially, if not exponentially, simpler than making the software be entirely correct. It is both true that software is a streaming pile of bugs, where the vast, vast majority of responses to possible inputs is somehow wrong, yet the vast, vast majority of inputs actually processed by the software are mostly correct (not entirely, but mostly) because they are in the generally polynomial subsets of the exponentially complicated space that the developers made correct... ish.

sansnomme 7y ago
To expand on this, floating point works for 95% of programs. It is the 5% that needs exact accuracy/precision offered by arbitrary precision libraries. Most programs hardly exhaust the entire range of your typical floating point usage range. For example in a GUI you won't be able to easily tell the difference between 100% and 99.9999999% by eyeballing.
vonseel 7y ago
I think I’ll use your comments as a response next time someone calls me out in a code review or says I deployed a bug. Specifically the polynomial exponentially complicated bits. The look on their faces would be priceless. And they would forever think I’m a jerk... since they wouldn’t get the sarcasm lol.
hcs 7y ago
This is why model checking and directed fuzzing are so effective! There are situations so stupid only a machine, or reality, could come up with them.

wyager 7y ago

> How did software get so reliable Talk about begging the question!

pjscott 7y ago
How many HTTP request does nginx usually serve before crashing? How long can a Linux kernel stay up before panicking? Some complex software is startlingly reliable.

AnimalMuppet 7y ago

1. Proof costs. Like, a lot. If you don't need the reliability, why would you pay for it? 2. How much reliability is needed? Not 100% (usually). If my OS crashes, I'm unhappy. If the OS on my company's production server crashes, that's a lot worse. But our production server is actually a redundant cluster, so if one machine crashes, people are unhappy, but nothing horrible happens. (In point 1, I talked about the cost of proven-to-be-perfect software. Needing to have a redundant cluster is part of the cost of not having perfect software, which also must be considered. But because the hardware isn't 100% reliable either, we needed a redundant cluster anyway...) 3. Formal methods are often playing catch-up. Now we have to worry about timing side-channel attacks through the cache. There may now be formal methods to prove that such things are not possible in a piece of software; I'm pretty sure there were not such formal methods five years ago. We keep finding new areas that can fail. (One advocate of formal methods replied to me some weeks ago that formal methods proved that the software would never do anything that it wasn't specified to do. I doubt that claim with respect to something like side-channel attacks. Even if it's true, though, I suspect that often the specification didn't include "no side channel attacks" until certain recent events brought it to more popular attention.) Proofs are therefore suffering from a double whammy: Not only are they painfully difficult and expensive, but they're incomplete. When something comes up that wasn't covered by the proof of correctness, you now need to fix it. And then you have to re-run all the proofs all over again, because your fix may have invalidated them. 4. All proofs have to start somewhere, usually with a formal specification. If the specification is wrong (looking at you, MCAS), all the formal proofs in the world won't save you. (Well... a system-level formal proof might. But that's even harder and more expensive. And even that fails if the system spec is flawed.) TL;DR: Real proofs are too expensive for the benefit they provide, in almost all cases. The cost-benefit just isn't there. Hope lies in making them easier and more automated to use (better type systems, for example).

panic 7y ago

How did proof itself get so reliable? The process of convincing yourself that a proof is correct isn't so different from the process of convincing yourself that a program is correct.

hcs 7y ago
And equivalently, if you had heavily-relied-on proofs that were as narrowly read and hard to follow as software, mathematics would be in just as bad a state.
garmaine 7y ago
Yes, it is. This can be shown with theory: proving a program is correct is NP-hard, but verifying the proof is in P-space. It is way easier to show a proof is correct than to generate the proof in the first place.
- panic 7y ago
  True, at least for formal proofs. I was thinking more of traditional mathematical proofs, which are often as hard to formalize as programs are to prove correct. In both cases, convincing yourself that the proof or program is correct involves reading it and seeing whether each of its parts follows from or fits into the other parts to make a coherent whole. Of course, there are ways to fool the reader, but I think people learn to avoid writing in ways that are likely to mask errors (e.g., not reusing the same symbol to mean completely different things, both in proofs and in programs).

gandalfgeek 7y ago

Short explainer video covering Hoare's original paper: https://youtu.be/eY8AyCZ5uUg https://youtu.be/eY8AyCZ5uUg

hcarvalhoalves 7y ago

The most trivial software system you can think of nowadays is already so large in scope and/or complex that you can’t prove it doesn’t work either, because there’s no complete specification on how it’s supposed to work - if it existed, it would be the bug-free software itself, because all software is specification. In the end all that matters is whether the system is useful, in an economical sense (value delivered > defects over time). So I would argue software did not get reliable, our bar for defects remained low, but the relative value delivered increased a lot because software has amazing leverage.

hcs 7y ago
Moreover, when you get an existence proof of a bug, it's usually easy to change such a system to seem ok. As Hoare also said, "There are two methods in software design. One is to make the program so simple, there are obviously no errors. The other is to make it so complicated, there are no obvious errors."

_bxg1 7y ago

Fascinating how perception has changed since then; I think most people today would have the opposite sentiment: "How did software get so unreliable?" My guess is: software creation and distribution became exponentially more accessible around that time (1996) with the advent of the web. Not only were many less-qualified individuals creating software (which isn't intrinsically a bad thing!), many more people were consuming software (making consumer software a much more lucrative market), and technology changes allowed companies to "move [much] fast[er] and break [more] things". Businesses were always optimizing for profits, and the dot com boom simply changed the equation to where reliability was no longer profitable in the majority of the field.

gelo 7y ago

Most of the software I have written for work has no near on no functional / unit tests. It is industrial process monitoring software that runs 247 on remote machines thousands of miles away. Simple fact is it has to work, no if's but's, even when there are faults in its environment. This does not mean to say that the software has not been tested. Testing is subjective to a softwares use. You could have 10000 tests and still have a series of bugs. Testing for my work comes as two categories, "Tested by design" and "Environmental Testing". "Tested by design" involves developing your software by which the designing and writing the software inherits the tests as you go. When I go about designing a feature, I expand on a chosen solution of that feature and then methodically branch out on the uses of that feature, build a map of dependancies, scenarios, outcomes, consequences etc for that feature. These become the basis of how I write the code for that feature because I have inherantly put in mitigations for everything I have considered before hand. There is no point in testing something excessively if you can and/or have garanteed by code that it will perform exactly as designed. That may seam a contraversial thing to say. With "Environmental Testing" we simulate the environment which the software is put into with real external factors. This is particular for the software I write. This is not always the best for another software project. I've written my works software from scratch 3 years ago and it has had various incremental additions and changes. Yes there have been bugs. I will admit that entirely. However the key thing with work's software is that is has rarely crashed or rarely faulted while containing those bugs. Most faults that have been found have been configuration errors/issues. I would be interested in how others approach testing strategies for the software they have written.

pjscott 7y ago

How does software get reliable at all, ever? In my experience there are two ways: 1. You write reliable software from the start. It feels a lot like writing a mathematical proof, or at least sketching one. After a few dumb bugs are fixed the code continues to work without issue, year after year, and nobody ever looks at it again. (This isn't as hard as it sounds! It's not the right approach for everything, but it should be more widely used than it is.) 2. You write normal software, i.e. unreliable crap, but you look at the ways that it goes wrong and fix them. This requires that you put some work into detecting that things have gone wrong. A lot of software companies will trace all crashes, and aggregate stack traces and logs from them. In this kind of environment, you can improve software reliability by sticking a paranoid number of assertions in your code and obsessively checking to see what triggered them. After a while all the common problems will have been removed, and the remaining bugs will be less prevalent than hardware failures -- and then you can declare victory.

pif 7y ago
From my experience, the problem with no. 1 is that, in order to build something correct, you have to know what you need to build, and that is a can of worms (actually, a snakes nest) that too many people refuse to address. The problem with no. 2, on the other side, is that it will eventually get correct, but you cannot predict when it will be reliable. And the same people who refuse to sign requirement documents are the same people who insist on having arbitrary deadlines.
- rstuart4133 7y ago
  > The problem with no. 2, on the other side, is that it will eventually get correct Actually, it doesn't necessarily get correct. There are old programs out where the ratio of bugs fixed by a modification / bugs introduced is less than 1. For small systems this never becomes a problem, but huge complex systems it really is a thing. The only way I know of to prevent it from happening is unit tests with excellent coverage and CI.
moksly 7y ago
In my experience the majority of enterprise service applications and smaller few-purpose systems are build following 1. We’ve have an ASP Web Forms food ordering system that’s basically four forms and a simple CRUD admin system page that’s been running flawless for half a decade. It’s only needed upgrades to its .NET system as we moved up the TLS version ladder, and it has thousands of daily users. There are no tests, no real monitoring outside of “is it still up?” and no complaints. Eventually we’ll have to clean up the database, eventually. But chances are someone will have build something new by then.

kazinator 7y ago

> How did software get so reliable without proof? Two words: survivorship bias! The software field exploded in the past half a century, producing a huge volume of activity producing a huge amount of cruft. A lot of the unreliable stuff gets shaken out; so what we see is a biased sample consisting of the successes that remain. Software that is halfway successful gets to be maintained, and over many years or decades, the reliability improves.

buzzkillington 7y ago

The main reason I've found for programs being 'correct' is that the range of actual inputs for programs is severely limited. Most programs see inputs that are similar enough to previous inputs that the latent bugs are never triggered, or at worst triggered one at a time. Running programs far outside their expected parameters on the other hand has nearly always lead to disaster.

amelius 7y ago
Would you say that a typical web-browser (a complicated piece of software) always sees the same kind of input?
- buzzkillington 7y ago
  Pretty much. Throwing [0] to chrome and firefox has made made them hang for 5 minutes so far. Generating the HTML took under a second and 13MB, large, but not larger than the fatter webpages out there. In terms of input browsers don't see but should be able to parse you can't get much simpler than this. [0] In Guile2.x: (define print (lambda (x) (display x) (newline))) (define div-hell (lambda (n) (cond ((eq? n 0) (print "TEXT")) (else (print "<div>") (div-hell (- n 1)) (print "</div>"))))) (print "<html><header><title>DIV HELL</title></header><body>") (div-hell 1000000) (print "</body></html>")

justlexi93 7y ago

The same way bridges, aeroplanes and medicine happened. What makes software so special?

tus88 7y ago

Fixed a ton of bugs. And it's not that reliable, and super reliable software in airplanes is proved.

aprdm 7y ago

Having worked in some places that aren't software companies it is pretty incredible how something a developer who is no longer in the company set in the last decade is still kicking ass with no monitoring or documentation. It's truly remarkable! All those databases that software depend on and go without people even realizing they exist until someone literally decomissions a datacenter only then to figure out lots of apps require that particular machine to be running... they're day in and day out working with 0 maintenance for years... impressive. Postgres, mysql and mongodb are examples of databases I've seen like that! As well as inhouse apps that depend on those databases... at most they have a cron job for backing up and keeping at most the last X backups.

speedplane 7y ago

This article misses the elephant in the room: how to define "reliability". Most software perceived to be reliable (eg, MS Paint, bash) have numerous bugs, it's just that no one comes across them. Software that is perceived to be "reliable enough" (eg, MS Word, Chrome), have bugs that pop up regularly. Here are some vague uptime reliability measures and what you need to get there: - 70% reliability: you can often just free-code it and pray. - 95% reliability: you better have a bunch of tests. - 99.5%: you need automated testing, coverage tools, documentation, team coordination tools, and and solid merge/deployment process. - 99.99%: all-of-the-above plus tests that aggressively attack and analyze production systems (eg, Netflix Chaos Monkey), coverage tests that do branch coverage and not just line coverage, simulating network failures, and/or test on a variety of hardware and user-configurations. - 100%: The only way to be absolutely certain, is to convert each line of code into a mathematical operator and solve for a formal proof of correctness. The 100% reliability standard is not just theoretical. The U.S. government issues software standards for safety critical devices (military, aviation, healthcare), and some of them do indeed require mathematical proof of correctness (EAL6+ being a key standard). They generally do not require 100% bug-free code, but just that some particular features are 100% bug free (e.g., the OS/scheduler will never deadlock).

yaantc 7y ago
> and some of them do indeed require mathematical proof of correctness > (EAL6+ being a key standard) Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS. [1] https://www.commoncriteriaportal.org/products/ https://www.commoncriteriaportal.org/products/
- speedplane 7y ago
  > Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS. You are definitely correct. Also, disclosure... I worked on that EAL7 Virtual OS. When I left it was only EAL6+, likely leading to my bias towards it.

otabdeveloper4 7y ago

If you compare K&R C and C++17, everything that has been added is some form or another of 'proofs'. So I take issue with the 'without proof' part; even if they're not proofs that adhere to strict mathematical forms, they're still there.

LoSboccacc 7y ago

most software today is a mess. only when you include the user in the loop with his version-3-new-final backups and willingness/need to retry in the event of error you get something that's workable. we've effectively shifted partial blame on the users, the famous "operator error" class of bugs, made sure to help then save often and substituted reliability with resilience but it doesn't mean software is reliable. the whole system as a whole and including users corrective actions is somewhat resilient enough for productive work

lngnmn1 7y ago

Exactly the same way as life itself got so reliable - by trial and error and selection of what is stable. /thread

tzjmetron 7y ago

Software is as reliable as the world we live in - basically, unreliable. Does that matter though? Practically, no. If it works well enough, it's good enough.

cjfd 7y ago

By fixing everything that goes wrong noticeably and by having no idea that many features are currently actually not working as they are supposed to? To actually create reliable software currently the best bet is to have automated tests for as many things as possible and exploratory manual testing around any feature that changes.

hannob 7y ago

I think the answer to the question posed may just be "it's like natural selection". A lot of software is horrifically bad. But not all flaws are created equal. A software that runs an online shop, but crashes 50% of the time during checkout will probably not create a successful company and thus won't survive long. However a software that has comparably many flaws and fails in all kinds of rare corner cases, but still gets the job done in most average cases, may just survive, even though it's equally bad.

p0nce 7y ago

How did people get the impression software was so reliable?

crimsonalucard 7y ago

>The problem with the question “How did software get so reliable without proof?” is that it’s asking the wrong question. It’s not that software got so reliable without proof: it’s that systems that include software got so reliable without proof. No. This person isn't sounding smart enough. The real question isn't how systems that include software got reliable without proof but instead the reverse: how did software that includes systems get so reliable without proof? That's how you should conclude an article with some hand wavy technical jargon.

amelius 7y ago

> How did software get so reliable without proof? Because most software is just moving data from one place to another, combined with some very simple business logic.

qubex 7y ago

What strikes me in both the original article and the post is the failure to recognise that a strong form of selective pressure is being applied upon software, and that adaptive processes (of which evolution is but a single example) tend to optimise for the criterion that is being selected for even in absence of an overarching design (‘proof’). I recommend reading Darwin Among the Machines for comparison to hardware.

jacquesm 7y ago

I don't think software is all that reliable. Almost every piece of major software that I use has one or more bugs and periodically locks up or crashes. We as users have been conditioned to accept this with the situation getting worse rather than better over the years. The main reason software seems more reliable than in the past is because in a SaaS environment the crash doesn't happen on your computer anymore. But the effect is the same unless extreme care was taken on the server side to ensure that no data was lost. In most cases we perform the equivalent of a reboot or retry: we reload the page.

shekharshan 7y ago

When it comes to writing reliable software the best paper I have read is “Design By Contract”. That one paper combined with proper usage of exceptions will go a long way in preventing bugs. Of course there is also a need for more rigor in requirements.

rkagerer 7y ago

It didn't.

egberts1 7y ago

Richard Feynman said it best: 1. Write down the problem 2. Think real hard 3. Write down the solution http://wiki.c2.com/?FeynmanAlgorithm http://wiki.c2.com/?FeynmanAlgorithm

waynesonfire 7y ago

See Betteridge's law of headlines.