I didn't like the essay much. The comparison with medeival medicine is a little shallow. One big problem he misses, is that unlike medeival medicine, computer science theory is well developed. CS has a solid theoretical foundation. The schism between engineers and academics mainly comes from the fact that "formal verification methods" are either not acheivable in practice, or require constraining a problem to a point where the verified software is not useful for anything.
Formal verification requires "ground truth". Something external that defines what the program should do, exactly. That's possible in some cases (a CPU emulator, for example, can be verified against a physical CPU). Most of the time, however, that doesn't exist.
That means what's usually necessary is a formal description of a formal semantics. Those things, almost universally, require either creating a Turing Complete semantic description language (to allow the semantics to be rich enough to express the solution), or a verry simple problem domain.
In the Turing Complete case, the formal spec degenerates to the program. That leaves you in a case where you are proving that the program does what the program does, which is useless.
The problem with simple domains is that they violate the law of leaky abstractions. All abstractions leak. Simple domains can rarely solve real problems. This is true even for cases like bison and flex. There is a reason most compilers use hand written parsers: they need to be usable by people. Once you move away from "I want a Boolean function that says if string S is in language Y" to "I want to provide usefull error output that helps people figure out the mistakes they have made, and I want to provide contextually relevant assistance in authoring code" the formal model falls apart.
So my prediction is this:
"Attempts to raise the level of abstraction (provided it's possible to escape to lower levels), will succeeded. Formal verification, however, is a myth".
Formal verification requires "ground truth". Something external that defines what the program should do, exactly. That's possible in some cases (a CPU emulator, for example, can be verified against a physical CPU). Most of the time, however, that doesn't exist.
That means what's usually necessary is a formal description of a formal semantics. Those things, almost universally, require either creating a Turing Complete semantic description language (to allow the semantics to be rich enough to express the solution), or a verry simple problem domain.
In the Turing Complete case, the formal spec degenerates to the program. That leaves you in a case where you are proving that the program does what the program does, which is useless.
The problem with simple domains is that they violate the law of leaky abstractions. All abstractions leak. Simple domains can rarely solve real problems. This is true even for cases like bison and flex. There is a reason most compilers use hand written parsers: they need to be usable by people. Once you move away from "I want a Boolean function that says if string S is in language Y" to "I want to provide usefull error output that helps people figure out the mistakes they have made, and I want to provide contextually relevant assistance in authoring code" the formal model falls apart.
So my prediction is this:
"Attempts to raise the level of abstraction (provided it's possible to escape to lower levels), will succeeded. Formal verification, however, is a myth".