5 ms·

Hmm. The paper argues that a predicted software crisis caused by unreliability didn't materialise, and software became tremendously more reliable, despite indus

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.
setr 8y ago

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.

setr 8y ago