9 ms·

How did software get so reliable without proof? (1996) [pdf]

83 points by elcapitan 8y ago

repolfx 8y ago
Hmm. The paper argues that a predicted software crisis caused by unreliability didn't materialise, and software became tremendously more reliable, despite industry essentially ignoring decades of research into formal methods and proof systems. With this I agree. I'd also contribute another couple of factors that came into play perhaps too late for a paper written in 1996: successfully bringing garbage collection and managed memory languages to widespread usage, starting with Java and JavaScript and the growth of the web that allowed much more software to be written in server side scripting languages like Perl and Python. And the deployment of crash reporters and online update tools, which massively tightened the feedback loop between crashes occurring in the wild and fixes being deployed. Intuitively at least, I feel these two things made a huge difference to the reliability and scalability of software. It's typical for large Java or JavaScript programs to now incorporate so many libraries that dependency version management is a significant pain point that is bottlenecking the growth in software complexity. In the 1990s the closest you got to this was DLL hell and that was more of a Windows deployment issue - the software worked fine on the developer's box, it just didn't work when deployed to OS installs that had different bits on the. Now we face issues where dependency graphs can pull in two or even three different incompatible versions of the same library on the developer's machine. This is a testament to the new scales we are exploring in software complexity. However, the paper then goes on to make some possibly very dubious arguments, I suppose because the author is a famous academic and maybe doesn't want to contemplate the obvious conclusion. He says: The conclusion of the enquiry will be that in spite of appearances, modern software engineering practice owes a great deal to the theoretical concepts and ideals of early research in the subject; and that techniques of formalisation and proof have played an essential role in validating and progressing the research. However, technology transfer is extremely slow in software, as it should be in any serious branch of engineering. Because of the backlog of research results not yet used, there is an immediate and continuing role for education, both of newcomers to the profession and of experienced practitioners. The final recommendation is that we must aim our future theoretical research on goals which are as far ahead of the current state of the art as the current state of industrial practice lags behind the research we did in the past. Twenty years perhaps? This is a very problematic set of conclusions which speaks to more general concerns growing in my mind in recent times about the value of much academic research. Because of course, it's now more than 20 years since C.A.R. Hoare wrote this, and yet formal methods are no more used now than they were in 1996. It's not that there's a backlog of research that isn't used. It's that academia has gone down this rabbit hole for decades and it has never been widely used. 40 years and hardly any success! Why would anything be significantly different given another 20? The paper does an admirable job of trying to congratulate everyone, whilst putting a brave face on lack of adoption - saying that a 20 year lag time between research and adoption is perfectly reasonable and a sign of maturity in the software industry. With another 20 years of hindsight, we can perhaps see now that industrial practice isn't lagging behind academic research, when it comes to formal methods and proofs. It's written it off and ignored it for good. The closest industrial practice gets to this is we use slightly stronger type systems now, but nothing a programmer teleported from 1996 wouldn't recognise.
- slededit 8y ago
  Formal methods have seen adoption in hardware where the cost of bugs is much higher. The fact is it’s cheaper to patch buggy software than it is to apply formal methods. Quality has remained above a level that would impede progress, and basically it just isn’t that big of an issue. On a smaller scale it’s been used in code checkers to find uses of uninitialized variables and “can be null” errors. Just in a limited form.
  - repolfx 8y ago
    I used to believe that was true, but recently I read that even in the hardware space formal methods have limited application - like software, they're usually used only on very specific sub-parts like MESI protocols. But it's not the case that a modern CPU is extensively applying formal methods. W.R.T. things like static type systems, I agree. But progress there has been fairly minimal in the widely adopted languages. Mostly, in fact, the type systems did not get stronger, but the focus was on making them easier to use through more type inference.
    - slededit 8y ago
      Full top down proofs are rare but it’s more common at the module level.
- toast0 8y ago
  I've been doing software for at least 20 years now, and occasionally heard about formal methods (a class I narrowly dodged while getting my BS in Computer Engineering); it seems like formal methods can approach proving you've followed the specifications. However, I've rarely actually had specifications, much less specifications that were complete or even relatively static. I think there's some value in formal methods for baseline things that could have formal specifications, things like schedulers, compilers, optimizers (maybe just enough to show that the optimizer didn't make anything worse), filesystems (although fairly complex), etc. But applications are way too wishy-washy most of the time to even have a spec, let alone something that would hold still long enough to verify.
- 8y ago
threatofrain 8y ago
As a small data point I'd say that Leslie Lamport claims that Amazon has used TLA+ on a good number of big projects; many people think of formal proving as an activity that is separately layered on top of programming, as opposed to a proving-language. Also, when people use Rust, are they using proving techniques?
- steveklabnik 8y ago
  Not yet; we’re still working on the semantics of the language, and proofs for it; you need that before you can prove things about the code in the language. Or at least, the stuff we’re most interested in. The EU is funding some of this work.
  - timClicks 8y ago
    For people interested in looking deeper, this work is called RustBelt. Useful web pages are the project's homepage (https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/) and the research paper describing the project (https://dl.acm.org/citation.cfm?doid=3177123.3158154&preflayout=flat https://dl.acm.org/citation.cfm?doid=3177123.3158154&preflay...)
- snaky 8y ago
  If you are interesting in a programming language suitable for system level programming, and using proving techniques, maybe ATS would be of interest. https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko https://bluishcoder.co.nz/tags/ats/index.html https://bluishcoder.co.nz/tags/ats/index.html
exabrial 8y ago
1996 being the pre Windows 98 Era
jedharris 8y ago
Thanks for this! Hoare (partially) answers a question I asked in the comments on "The Little Typer" (a good treatment of programming with dependent types). That approach to dependent types brings our code closer to being verifiable. Unfortunately as a number of commenters testified it also makes software (currently) impossible to scale to complex algorithms, dependence on loosely coupled libraries, and so forth. Since Hoare wrote 22 years ago, I'm now wondering if there's a fundamentally intractable problem with improving formal validation of complex software. Dependent types seem like a natural way of embedding the programmer's assumptions and reasoning into software, but clearly current technology in that area is still very very far short of helping with software at current scale. Meanwhile our practical means of building complex software have improved considerably and we can develop systems that are reliable "enough", even at enormously greater scale than Hoare anticipated. The gap between viable software complexity and formal methods of describing software semantics has grown much wider since Hoare, rather than shrinking. I wonder if we could step back from this style of formal methods, and look for an alternative approach. We need ways to capture the actual reasoning and methods that work for programmers building complex systems -- rather than trying to pretend they are mathematical objects.
- mikekchar 8y ago
  For me, notation is everything. A computer program is a model of a problem. There is more than one representation of that problem: in the static code and in the running code. If you go to a kind of naive way of writing programs (that we all went through when we were first starting out), you write the code and then you step through it (either on paper, or with a debugger), viewing how the code is running. There are many techniques available for helping you reason about your code. However, it's important to understand that software code is a notation for modelling the problem. Often formal methods introduce another notation that proves that the encoding of the problem in the first notation is "correct" according to some definition of "correct". The more we move into modelling the correctness in the second notation, the more we move the burden of reasoning about the issue to the "code" in the second notation. It's often very useful to model the problem more than once. For example, I'm quite a big fan of unit tests. "Give the code in the system, I expect X to be true/false in this situation". I'm just as likely to make mistakes in my unit tests as I am with the production code. However, it's the comparison of the two that allows you to reason effectively about the code. They are two sides of the same coin (intentionally coupled -- which, as an aside, is why you should avoid trying to decouple your tests from your production code!!!). Even though it is useful to model twice, I'm not really sold on the idea of doing it in general (and I have a very specific idea of how to write unit tests that's heavily coloured by this point of view). Everything that you add to the code should make reasoning about something easier and more convenient than not doing it. Otherwise you are better off with just writing the production code. You will have less complexity to deal with overall. In my opinion, a good example of a tool that helps incredibly well are strongly typed languages with type inference systems. For a small penalty of type notation, the system can tell me, without a doubt, when I've made a mistake with the types of my variables. Not only that, but the notation itself allows me to reason about why I've gotten myself into a problem. It can even help me reason about what the function does, without having to even look at the implementation. This is incredibly helpful. I think as we go forward, we need to be looking for this kind of tool. Dependent types seem like a perfect example of this. However, there is always going to be a small price to pay. Writing code in a statically typed language is harder than writing code in a dynamically typed language -- precisely because the dynamically typed language allows you to write code without having to think up front about the consequences. Of course, you may leave bugs in your code because of it, but the initial cognitive load is smaller. Similarly, it's much better to write code where you can reason about the run time behaviour without it running, but that is much harder than writing some code and walking through it, playing "computer". We need to balance these kinds of factors because a tool that is not used is a useless tool. I'd be perfectly happy to work in a pure functional, statically typed language because it is much easier to reason about my code. Many of my colleagues simply are not willing (or possibly even able) to pay the upfront cost of working in that kind of ecosystem. Hence, I'm not able to work in it either.
nikofeyn 8y ago
was 1996 really that different than today? because reliable is the last word i would use to describe software today.
- ashleyn 8y ago
  The internet wasn't as big and software frequently shipped as a boxed product on a disk, cartridge, or CD-ROM. You had one shot to get it right without major bugs because fixing them required another run of physical media.
- passwd 8y ago
  It surely is different. We at least managed to contain some of the issues in normal operation. Back in the day, crashing whole OS in BSOD/panic style was more common, drivers unstable, things written in not-so-safe languages more popular. So ultimately it depends what do you mean by reliable - by itself, functionality might not be so much better, but yes, sometimes you don't mind as much as you would do back then.
- patrickg_zill 8y ago
  There was more Pascal and more assembly language. Some believe that Macintosh suffered a lot of instability from the switch to C from Pascal. I don't have any source code to point to however, only anecdote.
- 2sk21 8y ago
  Even in the late 90s, source code revision control was a dark art: either you used extremely expensive proprietary systems or else you used CVS which was very low level and completely lacked integration with any bug tracking system. Merging in a big feature in CVS was a nerve-racking experience.
lngnmn1 8y ago
Same as life itself - by trial-and-error with feedback loops and backprop.
grandinj 8y ago
We've gotten to where we are using slow incremental improvements. Better tools, better compilers, vastly better linters, unit testing, CI, etc. Now and then we manage to take some academic research and turn it into practible stuff e.g. the current generation of linters like FindBugs, Coverity, etc. And that is pretty much as it has always been, a slow drip of practical improvements fed by theoretical research.

83 points by elcapitan 8y ago

Hmm. The paper argues that a predicted software crisis caused by unreliability didn't materialise, and software became tremendously more reliable, despite industry essentially ignoring decades of research into formal methods and proof systems. With this I agree. I'd also contribute another couple of factors that came into play perhaps too late for a paper written in 1996: successfully bringing garbage collection and managed memory languages to widespread usage, starting with Java and JavaScript and the growth of the web that allowed much more software to be written in server side scripting languages like Perl and Python. And the deployment of crash reporters and online update tools, which massively tightened the feedback loop between crashes occurring in the wild and fixes being deployed. Intuitively at least, I feel these two things made a huge difference to the reliability and scalability of software. It's typical for large Java or JavaScript programs to now incorporate so many libraries that dependency version management is a significant pain point that is bottlenecking the growth in software complexity. In the 1990s the closest you got to this was DLL hell and that was more of a Windows deployment issue - the software worked fine on the developer's box, it just didn't work when deployed to OS installs that had different bits on the. Now we face issues where dependency graphs can pull in two or even three different incompatible versions of the same library on the developer's machine. This is a testament to the new scales we are exploring in software complexity. However, the paper then goes on to make some possibly very dubious arguments, I suppose because the author is a famous academic and maybe doesn't want to contemplate the obvious conclusion. He says: The conclusion of the enquiry will be that in spite of appearances, modern software engineering practice owes a great deal to the theoretical concepts and ideals of early research in the subject; and that techniques of formalisation and proof have played an essential role in validating and progressing the research. However, technology transfer is extremely slow in software, as it should be in any serious branch of engineering. Because of the backlog of research results not yet used, there is an immediate and continuing role for education, both of newcomers to the profession and of experienced practitioners. The final recommendation is that we must aim our future theoretical research on goals which are as far ahead of the current state of the art as the current state of industrial practice lags behind the research we did in the past. Twenty years perhaps? This is a very problematic set of conclusions which speaks to more general concerns growing in my mind in recent times about the value of much academic research. Because of course, it's now more than 20 years since C.A.R. Hoare wrote this, and yet formal methods are no more used now than they were in 1996. It's not that there's a backlog of research that isn't used. It's that academia has gone down this rabbit hole for decades and it has never been widely used. 40 years and hardly any success! Why would anything be significantly different given another 20? The paper does an admirable job of trying to congratulate everyone, whilst putting a brave face on lack of adoption - saying that a 20 year lag time between research and adoption is perfectly reasonable and a sign of maturity in the software industry. With another 20 years of hindsight, we can perhaps see now that industrial practice isn't lagging behind academic research, when it comes to formal methods and proofs. It's written it off and ignored it for good. The closest industrial practice gets to this is we use slightly stronger type systems now, but nothing a programmer teleported from 1996 wouldn't recognise.

slededit 8y ago
Formal methods have seen adoption in hardware where the cost of bugs is much higher. The fact is it’s cheaper to patch buggy software than it is to apply formal methods. Quality has remained above a level that would impede progress, and basically it just isn’t that big of an issue. On a smaller scale it’s been used in code checkers to find uses of uninitialized variables and “can be null” errors. Just in a limited form.
- repolfx 8y ago
  I used to believe that was true, but recently I read that even in the hardware space formal methods have limited application - like software, they're usually used only on very specific sub-parts like MESI protocols. But it's not the case that a modern CPU is extensively applying formal methods. W.R.T. things like static type systems, I agree. But progress there has been fairly minimal in the widely adopted languages. Mostly, in fact, the type systems did not get stronger, but the focus was on making them easier to use through more type inference.
  - slededit 8y ago
    Full top down proofs are rare but it’s more common at the module level.
toast0 8y ago
I've been doing software for at least 20 years now, and occasionally heard about formal methods (a class I narrowly dodged while getting my BS in Computer Engineering); it seems like formal methods can approach proving you've followed the specifications. However, I've rarely actually had specifications, much less specifications that were complete or even relatively static. I think there's some value in formal methods for baseline things that could have formal specifications, things like schedulers, compilers, optimizers (maybe just enough to show that the optimizer didn't make anything worse), filesystems (although fairly complex), etc. But applications are way too wishy-washy most of the time to even have a spec, let alone something that would hold still long enough to verify.
8y ago

threatofrain 8y ago

As a small data point I'd say that Leslie Lamport claims that Amazon has used TLA+ on a good number of big projects; many people think of formal proving as an activity that is separately layered on top of programming, as opposed to a proving-language. Also, when people use Rust, are they using proving techniques?

steveklabnik 8y ago
Not yet; we’re still working on the semantics of the language, and proofs for it; you need that before you can prove things about the code in the language. Or at least, the stuff we’re most interested in. The EU is funding some of this work.
- timClicks 8y ago
  For people interested in looking deeper, this work is called RustBelt. Useful web pages are the project's homepage (https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/) and the research paper describing the project (https://dl.acm.org/citation.cfm?doid=3177123.3158154&preflayout=flat https://dl.acm.org/citation.cfm?doid=3177123.3158154&preflay...)
snaky 8y ago
If you are interesting in a programming language suitable for system level programming, and using proving techniques, maybe ATS would be of interest. https://www.youtube.com/watch?v=zt0OQb1DBko https://www.youtube.com/watch?v=zt0OQb1DBko https://bluishcoder.co.nz/tags/ats/index.html https://bluishcoder.co.nz/tags/ats/index.html

exabrial 8y ago

1996 being the pre Windows 98 Era

jedharris 8y ago

Thanks for this! Hoare (partially) answers a question I asked in the comments on "The Little Typer" (a good treatment of programming with dependent types). That approach to dependent types brings our code closer to being verifiable. Unfortunately as a number of commenters testified it also makes software (currently) impossible to scale to complex algorithms, dependence on loosely coupled libraries, and so forth. Since Hoare wrote 22 years ago, I'm now wondering if there's a fundamentally intractable problem with improving formal validation of complex software. Dependent types seem like a natural way of embedding the programmer's assumptions and reasoning into software, but clearly current technology in that area is still very very far short of helping with software at current scale. Meanwhile our practical means of building complex software have improved considerably and we can develop systems that are reliable "enough", even at enormously greater scale than Hoare anticipated. The gap between viable software complexity and formal methods of describing software semantics has grown much wider since Hoare, rather than shrinking. I wonder if we could step back from this style of formal methods, and look for an alternative approach. We need ways to capture the actual reasoning and methods that work for programmers building complex systems -- rather than trying to pretend they are mathematical objects.

mikekchar 8y ago
For me, notation is everything. A computer program is a model of a problem. There is more than one representation of that problem: in the static code and in the running code. If you go to a kind of naive way of writing programs (that we all went through when we were first starting out), you write the code and then you step through it (either on paper, or with a debugger), viewing how the code is running. There are many techniques available for helping you reason about your code. However, it's important to understand that software code is a notation for modelling the problem. Often formal methods introduce another notation that proves that the encoding of the problem in the first notation is "correct" according to some definition of "correct". The more we move into modelling the correctness in the second notation, the more we move the burden of reasoning about the issue to the "code" in the second notation. It's often very useful to model the problem more than once. For example, I'm quite a big fan of unit tests. "Give the code in the system, I expect X to be true/false in this situation". I'm just as likely to make mistakes in my unit tests as I am with the production code. However, it's the comparison of the two that allows you to reason effectively about the code. They are two sides of the same coin (intentionally coupled -- which, as an aside, is why you should avoid trying to decouple your tests from your production code!!!). Even though it is useful to model twice, I'm not really sold on the idea of doing it in general (and I have a very specific idea of how to write unit tests that's heavily coloured by this point of view). Everything that you add to the code should make reasoning about something easier and more convenient than not doing it. Otherwise you are better off with just writing the production code. You will have less complexity to deal with overall. In my opinion, a good example of a tool that helps incredibly well are strongly typed languages with type inference systems. For a small penalty of type notation, the system can tell me, without a doubt, when I've made a mistake with the types of my variables. Not only that, but the notation itself allows me to reason about why I've gotten myself into a problem. It can even help me reason about what the function does, without having to even look at the implementation. This is incredibly helpful. I think as we go forward, we need to be looking for this kind of tool. Dependent types seem like a perfect example of this. However, there is always going to be a small price to pay. Writing code in a statically typed language is harder than writing code in a dynamically typed language -- precisely because the dynamically typed language allows you to write code without having to think up front about the consequences. Of course, you may leave bugs in your code because of it, but the initial cognitive load is smaller. Similarly, it's much better to write code where you can reason about the run time behaviour without it running, but that is much harder than writing some code and walking through it, playing "computer". We need to balance these kinds of factors because a tool that is not used is a useless tool. I'd be perfectly happy to work in a pure functional, statically typed language because it is much easier to reason about my code. Many of my colleagues simply are not willing (or possibly even able) to pay the upfront cost of working in that kind of ecosystem. Hence, I'm not able to work in it either.

nikofeyn 8y ago

was 1996 really that different than today? because reliable is the last word i would use to describe software today.

ashleyn 8y ago
The internet wasn't as big and software frequently shipped as a boxed product on a disk, cartridge, or CD-ROM. You had one shot to get it right without major bugs because fixing them required another run of physical media.
passwd 8y ago
It surely is different. We at least managed to contain some of the issues in normal operation. Back in the day, crashing whole OS in BSOD/panic style was more common, drivers unstable, things written in not-so-safe languages more popular. So ultimately it depends what do you mean by reliable - by itself, functionality might not be so much better, but yes, sometimes you don't mind as much as you would do back then.
patrickg_zill 8y ago
There was more Pascal and more assembly language. Some believe that Macintosh suffered a lot of instability from the switch to C from Pascal. I don't have any source code to point to however, only anecdote.
2sk21 8y ago
Even in the late 90s, source code revision control was a dark art: either you used extremely expensive proprietary systems or else you used CVS which was very low level and completely lacked integration with any bug tracking system. Merging in a big feature in CVS was a nerve-racking experience.

lngnmn1 8y ago

Same as life itself - by trial-and-error with feedback loops and backprop.

grandinj 8y ago

We've gotten to where we are using slow incremental improvements. Better tools, better compilers, vastly better linters, unit testing, CI, etc. Now and then we manage to take some academic research and turn it into practible stuff e.g. the current generation of linters like FindBugs, Coverity, etc. And that is pretty much as it has always been, a slow drip of practical improvements fed by theoretical research.