No matter how much I wish for formal methods to become more mainstream I’m going on the record to say that they’ll never be mainstream. It’s too much for the typical software engineer. The gap between what regular software engineering looks like and what formal methods look like is just too wide and I don’t think there is any simple or even complicated way to close that gap. There is an irreducible amount of complexity when it to comes to stating and proving theorems and the only system up to the task is the human brain. So far the neural net people haven’t figured out how symbolic reasoning works and formal methods are the domain of symbolic methods.

Here is an example of a theorem from one of the first few chapters of “Software Foundations”

Theorem filter_exercise : forall (X : Type) (test : X -> bool) (x : X) (l l' : list X), filter test l = x :: l' -> test x = true.

This theorem is intuitively true and the informal reasoning justifying it is pretty simple: if you filter some list with a predicate and then look at the resulting list then the head of that list must have satisfied the predicate because if it hadn’t then the predicate would have been false and it would have been filtered out, QED.

Unfortunately the formal proof is anything but that simple. In fact, if you try this exercise and look at the resulting proof term then it’s more lines than this entire post. Until formal methods get to the point where formal proofs are as simple as informal proofs there is no way any of this stuff will go mainstream.