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.