Recently, I’ve been thinking about how we describe research on program verification. Searching for papers in the ACM Digital Library that mention “Formal software verification” produces a large number of results, nearly 68,000 papers since 2012. Skimming through a few of them, I found papers ranging from proofs of compiler correctness (e.g., work related to the CompCert C compiler) to papers on “runtime verification,” a form of execution monitoring that has its own dedicated conference, with a wide range in between.

What’s clear is that “verification” is now an umbrella term describing work broadly related to improving software quality. That’s great! I hope that umbrella continues to broaden.

But, I also miss a more precise name that captures its original usage, i.e., proving a program correct against a mathematical specification of a wide class of its behaviors, including properties like functional correctness, various notions of security, computational complexity, program equivalence, and several others. Especially given much recent progress in this space, a more precise name would help communicate ideas more effectively and reduce the potential for misunderstandings. It doesn’t help that the word “verification” is also commonly used in contexts other than software quality. For example, this Google help page uses the word a half-dozen times in relation to confirming a user’s email address, and the image for this post suggests that “verification” is tantamount to “authentication.”

Program proof?

The particular flavor of program verification that some of my own work focuses on involves proving theorems about software implementations that cover functional and security properties, e.g., proving, say, that code implementing a cryptographic construction corresponds to a mathematical specification of its input/output behavior (ruling out algorithmic and coding errors), and that the code’s execution time does not depend on secrets (preventing certain classes of side channels).

This kind of work has for long been described as “program verification”—it certainly fits the description used by Boyer and Moore in their short 1985 paper titled “Program Verification.” But, to emphasize its difference from other kinds of software-quality improvements that are also called verification, I’ve started to refer to my work as “program proof,” including in another recent blog post.

I like “program proof” for a few reasons. First, it is relatively unfamiliar to most people not working in the field and carries little unforeseen baggage. Second, it has a long, distinguished tradition, e.g., Morris and Jones use it to describe work by Turing, McCarthy, Naur, Floyd, Hoare, Dijkstra and others. Third, it evokes the Curry-Howard correspondence between proofs and programs. Finally, it isn’t specific to proofs of functional correctness, since program proofs may also cover non-functional properties like computational complexity or security.

Terminology is hard, but education is worth it

I first posed the idea that we need a term more precise than “formal verification” in a post on my Facebook page. A lively discussion ensued! Many agreed that more precise names would be valuable, and some suggested different names, including the following:

• Proof engineering
• Mechanized proof
• Mathematical proofs of software correctness
• Full motherfunctional correctness (yes!)

Others suggested to keep using “program verification,” but to explain the value of program proof by placing it in contrast with testing. Others wondered whether a rebranding was needed at all—providing more context when using the term might be sufficient.

All these points are fair. I think a rebranding can be helpful, but I don’t feel strongly about it. Indeed, it’s rare that an attempted sharpening of terminology actually takes hold. In any case, with or without a new term, it’s clear to me that what’s really needed is a more concerted effort at educating people (even experts in nearby fields) about what program proofs really are. In my experience, some simply do not realize the magnitude of what today’s state-of-the-art processes and tools can achieve, e.g., full memory safety proofs of C programs, full functional correctness proofs of compilers and operating systems, and end-to-end security properties of distributed systems. Perhaps if this education commences using a new term, rather than an existing term and its baggage, the ideas will take hold and excite the imagination about what we have managed to achieve, and what more may yet come!

Bio: Nikhil Swamy is a Principal Researcher at Microsoft Research, in Redmond, WA. He works on various topics including software security, type systems, functional programming, program verification proof and interactive theorem proving, often applying his work to the F* programming language and proof assistant.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.