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.
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.
The fact that new notations/representations (be that tests, simulations, formal methods, etc.) must justify their additional cognitive overhead is a great point.
Aside from unit and integration tests, I think that substantial new notation/infrastructure is most justifiable when the second notation/setting allows you to model parts of the problem that can't be modeled in the original notation.
Embedded software is a good example. Although there are some tools that allow you to model the physical system alongside the control software, typically the code is written in C and so there's no way of expressing very important aspects of the problem in the implementation language. So a second notation can help. For example, simulators and HiL setups for testing or things like https://github.com/LS-Lab/KeYmaeraX-release for formal methods.
Security is another good example. Typically code does not include an explicit threat model or explicit security properties, and these aspects of the problem are often scattered across the code and difficult to reason about. So being able to capture those things directly in a second notation can add a lot. For example, automatic vulnerbaility scaners for testing or https://tamarin-prover.github.io/ for formal methods.
Distributed/fault-tolerant systems are yet another example where it's very hard to state the thing you want to state in the implementation language. Netflix's chaos monkey comes to mind.
We don't seem to have the same level of help yet with dependent types. A detailed comment in a Reddit thread: <https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_o... indicates that we still can't use them on large scale systems. This was some time ago but AFIK we still have all the problems listed.
I wonder if there's good work on inference of minimal dependent types for APIs etc. I am not very familiar with current work so would be very interested in getting references. It seems that deriving canonical minimal types would resolve a lot of the listed problems.
And that is pretty much as it has always been, a slow drip of practical improvements fed by theoretical research.
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.
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.
The EU is funding some of this work.
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.
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.
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.
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.
I think that academics ignored the cost of proofs. They said "This is the right way. You should do it this way." But industry said "This is really expensive. If we try to use it for everything, you're only going to get 1% as much software, if that." And that wasn't realistic for industry. There were customer needs (and money to be made meeting them). For the real world, formal methods are too expensive to be worthwhile (in all but a very few situations).
Try using any imperative language with integrated proof predicates like Dafny, Whiley, etc. You'll immediately notice that they struggle to understand even properties of the code that looks extremely obvious, for instance they require lots of loop annotations. The examples being proven correct all end up being so trivial that you can just as well prove them correct by simply reading and thinking about them.
In the functional space things are hardly better. Formal methods in FP has evolved into dependent types research. But dependent types are more or less dependent on functional languages - the flagship is Idris, which is based on Haskell. But Haskell and other pure FP languages have been around for decades. Despite being extensively promoted to students at universities around the world, these languages have not seen wide adoption, so it stands to reason dependent types can't either. And again, the sorts of things being proven tend to be fairly trivial.
The way industry is going is pretty clearly small improvements to existing type systems, in particular, implementing value types into managed languages so the costs of using strong types is lower, where otherwise raw/primitive types would be used. And there's a huge focus on tuning and improving generics, flow typing, type inference and other usability improvements.
In other words, industry practitioners don't believe lack of proving power is our problem. They believe we aren't using the power of the type (proof) systems we already have, because the usability is too low.
Are they? I attended a pretty good university in my EU country, and the only functional language teaching was a couple of weeks of OCaml. We had more time of Prolog than that, but 90% of the course was Java and C.
But they’re obviously not equivalent, and most businesses only care about correctness to a certain limit (at which point its superceded by other factors; diminishing returns and all that), then formal certains will naturally only appear in common use until they reach that limit.
But at the same time, is it the academic’s job to build practical systems, to advance industry? Isnt that the role of the industrial researcher? As I understood it, academia’s ideal role is to simply advance human understanding in interesting ways: whether it has immediate practical consequence should not be in their domain. ie research ML decades before it has any real hope of being useable. It’s industry itself who takes the role of poring over the academic’s work, and figuring out if they can use it for anything. And if its cost-effective.
And if industry specifically wants academia to look into things of immediate interest, they shouldn’t be waiting on universities for it; they should be hiring an academic to specifically research it.
Academia love to claim that practical application should not be any concern of theirs. But why should this be so? After all, they eat practical food and live in practical houses. Someone has to pay for it all. And the idea, espoused in this essay, that eventually, on a long enough timescale, their research will all be adopted and it's just that industry is super slow to recognise the awesomeness of their research and productize it - well, this claim seems to be getting weaker all the time. We now have many areas of computer science that have spent decades going down very expensive rabbit holes with no serious adoption and none on the horizon.
Not just formal methods, but pure FP languages like Haskell remain rarely adopted despite huge hype and massive academic investment. There was a few days ago, a post asking what happened to the semantic web with many commenters positing that the semantic web became an academic money pit that absorbed huge quantities of grant money and delivered nothing whatsoever. I'm sure there are many other examples lurking if you scratch the surface.
If academic funding was cut significantly and returned to companies in the form of lower corporation taxes, perhaps connected to research incentives, would it be so bad? There'd probably be less research done overall but if lots of current research goes nowhere and is never adopted that'd be a net win.
I'm not saying industry always gets it more right than academia, but I think even the orgs like Microsoft Research that are basically just clones of academia, are still on a slightly better path. For instance MSR has done a lot of cutting edge research into operating system design. Still, the money was in the end wasted - nothing of Midori ever surfaced in real products.
The gold standard for me is Google. They're one of the few firms that managed to completely fuse research and industrialisation into a totally cohesive whole. Whilst they technically speaking have a research department, the research they're known for is largely not done there and Google has managed in the past to routinely create new innovations from all over the company.
It's worth realising that a lot of industrial and corporate research isn't labelled as such. It's just "innovative product development".
Example: If we look at JetBrains, they developed a new programming language from scratch (Kotlin) that has several innovative and cutting edge features. Do we think of JetBrains as a sponsor of research or Kotlin as the product of research, probably not, yet it solves many problems that were previously unresolved, like how to make a new language that has seamless interop with Java, and how to improve the usability of features like generics and nullity checking. The work involved in creating it explored new frontiers that academia has ignored, simply because usability improvements and practical topics like interop with existing code is not considered 'smart' enough to be worth the title of research.
Now that is cutting edge but incredibly practical research that could have industry-shaking impact within the next 10 years. It isn't primarily funded by the NSF or EU though. It's funded by a corporation.
Yes and no. This is an engineering science. In a pure science, the world is out there to explore and find out about, constraining what you do. An engineering science is very much about useful things we can build and how we can get better at doing that. Buildings that stay up and house people/things, planes that can fly, ships that float, that sort of thing.
Without a world to find out about and without being constrained by stuff to build, things get a bit arbitrary. At that point, it's really more pure art than anything else. Math is sort of the exception where we allow that kind of freedom. Sabine Hossenfelder's Lost in Math is a reminder of the dangers of applying that approach to other disciplines.
Anyway, I think it is actually wrong to pin academia's irrelevance to this fundamental divide. The problems in industry aren't too easy / boring to be of interest to academics. They are too hard to be solvable by anyone with the current insane level of publication requirements.
Michael Stonebraker talked about this in detail:
It's a great talk.
The shop coder may have never heard of a formal method and thinks it is something that must be "slow" or "too complicated", but they inevitably come crashing into tools and techniques that were informed by formal methods. In the 80's it was hard to get your hands on a C compiler. In the 90's, everyone still thought that OOP was going to change everything. By the 00's we finally saw widespread adoption of garbage collected languages. And more recently we've had better package management and efforts to rework lower level coding.
We've never left behind cargo-culting, given the growth in the number of programmers, but the strides are there, always hovering a few steps behind the code that is considered the "production code". The production code is seen as far too fast moving to be considered for "formal methods", yet it still ends up using "design patterns", echoing Hoare's notes about defensive coding techniques. We don't "prove" our C++ code is good, but we run a "static analysis" tool or a "fuzzer" on it.
Perfect, the enemy of good enough.
But Hoare talks specifically about formal methods, which is widely understood to mean proving code meets a spec using techniques like constraint solvers. Dependent types may meet the definition too. And none of these techniques are used widely or have ever been used widely.