I think the author should have expanded a bit upon "extremely expensive to apply", because that phrase is technically true but really hides the actual problems with formal verification and why it is seldom used in practice.
People unfamiliar with formal verification think it means "the code is provably correct", but that's not what it does. Formal verification can prove that your code correctly implements a specified standard. You still have to define and write that standard. And that's where the problems begin:
- Standards themselves can have bugs, or the standard you wrote is not what you actually wanted. Note that this is the same problem that often occurs in code itself! You've just pushed it up a level, and into an even more arcane and less-debuggable language to boot (formal standards are generally much, much harder to write, debug, and reason about than code)
- The standard is constantly changing as feature requests come in, or the world around you changes. Modern software engineering mostly consists of changing what you or somebody else already built to accommodate new features or a new state of the world. This plays very badly with formal verification.
Formal verification can work in areas where you have a long time to do development, or where your problem space is amenable to having a formal standard (like math problems). In most other cases it just runs completely opposite to the actual problems that software engineering is trying to solve.
A lot of the types of formal methods that Hillel Wayne (the author) writes about are the opposite of what you describe—you write a specification which is provably correct, and then it's up to you to translate that specification into code. The error-prone part is the translation more than the specification.
It amounts to the same thing: it takes a long time to develop, the specification can get out of sync with the code, and once out of sync you now have no provable characteristics of the new system.
Though this does make me wonder: If there exist some formal methods that can prove that code implements a standard, and others that can prove that the standard is correct, it seems like there ought to be something in the middle that can prove both.
> Formal verification can work in areas where you have a long time to do
> development, or where your problem space is amenable to having a formal
> standard (like math problems). In most other cases it just runs completely
> opposite to the actual problems that software engineering is trying to solve.
Have you actually tried, or is this just the standard line?
I've heard this from people I've worked with, and when I followed up to ask what kinds of projects they've worked on with Agda, Idris, Coq, Lean, whatever, they had nothing.
I don't have anything either, other than that I've toyed around with some of these systems a little bit. But it seems to me like there's a lot of potential in dependently-typed programming, and we just don't have a lot of experience with it -- which is fine, but that's a very different situation than what seems to be the standard line, "all formal methods take a ton of time and are only viable in a few niche projects" (what are people imagining here? NASA space probes and stacks of binders? really it doesn't seem obvious to me, I'm not trolling).
I'm not sure I agree with your conclusion. There's a large grey area in the formal methods space where general software engineering thrives (in my opinion). Especially the "lightweight formal method" variety. I doesn't go for complete proofs, but instead pursues a style of exhaustive (or something that approximates it) checking. Going down this route puts a very positive design pressure on your applications as well as your thinking in general.
The big pay off in formal methods is learning to think abstractly (imho). Even if you don't make a full blown model, sketching out the problem in something like TLA+ can be extremely valuable just by forcing you to think about the modeling independently of code. Even in the world of general software engineering, being able to reframe requirements as temporal invariants has felt something like a super power.
People unfamiliar with formal verification think it means "the code is provably correct", but that's not what it does. Formal verification can prove that your code correctly implements a specified standard. You still have to define and write that standard. And that's where the problems begin:
- Standards themselves can have bugs, or the standard you wrote is not what you actually wanted. Note that this is the same problem that often occurs in code itself! You've just pushed it up a level, and into an even more arcane and less-debuggable language to boot (formal standards are generally much, much harder to write, debug, and reason about than code)
- The standard is constantly changing as feature requests come in, or the world around you changes. Modern software engineering mostly consists of changing what you or somebody else already built to accommodate new features or a new state of the world. This plays very badly with formal verification.
Formal verification can work in areas where you have a long time to do development, or where your problem space is amenable to having a formal standard (like math problems). In most other cases it just runs completely opposite to the actual problems that software engineering is trying to solve.