Why Proving Computer Program Correctness Isn’t Usually Practical

I think I first learned about mathematical proofs in my high school geometry class. We learned how to prove that two triangles are congruent using the side-angle-side theorem (“If two sides and the included angle of one triangle . . “)

Years later when I was a university professor, I taught classes in “software engineering” — the science of computer programming. A topic in those classes was functional programming languages like LISP and Prolog. One of the ideas motivating functional programming is that if you construct a program as a collection of functions without any side effects, it’s possible to “prove the program correct”.

Proving program correctness has remained an area of research. The idea is great in theory, but just isn’t practical in most scenarios. I’ve worked with several systems related to program correctness.

* The process of proving a program correct requires far more time and effort than writing the program. This means it’s only useful for one-off software systems (such as space flight) that have years of development time and huge budgets. Proving correctness is impractical for the majority of commercial application software systems.

* Proving a program correct is usually only feasible for small, relatively simple programs. But for such simple programs you really don’t need a formal proof of correctness. (But catastrophic bugs are still possible).

* To prove a program correct, you have to know what the goal/behavior of the program is. But that means you need a correct version of the program to begin with. (But it’s possible to prove parts of a system correct where correct means consistent in some sense).

A topic that’s closely related to proving program correctness is automated mathematical theorem proofs. This is also a topic that has been around for decades, but with very slow practical progress.

A colleague of mine alerted me to a math theorem proving system called Lean. See https://leanprover.github.io/theorem_proving_in_lean/introduction.html

Part of the documentation for the Lean project reads, “The Lean project was launched . . . in 2013. It is an ongoing, long-term effort, and much of the potential for automation will be realized only gradually over time.” In my mind this translates to, “We realize this is research and might take years to make progress.”

Note: I reached out via email to the original creator of the Lean system and asked him if the name “LEAN” was an acronym. He replied that, no, LEAN is not an acronym. The name incorporates a capital ‘E’, which when backwards is the logic “there exists”, and a capital ‘A’, which when upside down is the logic “for all”. Clever!

A screenshot from the Wikipedia entry on Lean. One problem with program and theorem provers is that they have very steep learning curves.

Theorem provers and program correctness have great potential but remain huge challenges. The fact that progress has been so slow suggests that the current approaches may never lead to a big breakthrough, and that such a big breakthrough might require a wildly new approach.

But sometimes slow, incremental improvement works — neural networks limped along for decades until 2015 when a combination of increased processing power, GPU-based tensor libraries such as PyTorch, improved algorithms such as Adam optimization, and increased data storage capabilities, all converged to enable a giant increase in neural network capabilities.

Several of my friends’ wives love the TV show “Dancing with the Stars”. The show is wildly popular and is shown in several different countries. Proving a theorem correct is one thing, but I’m not sure it’s possible to prove a dance routine is correct. Here are three examples from the TV show that I’m pretty sure would be labeled “not correct”.

This entry was posted in Miscellaneous. Bookmark the permalink.