The fundamental role of logic and proof in computer science

MIT Press recently published Fundamental Proof Methods in Computer Science, a book by Konstantine Arkoudas and David Musser, a professor emeritus of computer science at the Rensselaer Polytechnic Institute (RPI). The book puts proofs into practice, demonstrating the fundamental role of logic and proof in computer science.

For Arkoudas, a senior research scientist at Bloomberg, the book fulfills an eight-year commitment. It uses a programming language that he invented to explore proof techniques of central importance in computer science.  As Google’s director of research Peter Novig explains, the work is “a well-written inspirational manifesto explaining why it is important to be able to think about and work with proofs.” And noted C++ programmer Alexander Stepanov, co-author of The Elements of Programming, wrote that his “professional life would have been easier had this book been available” when he was starting out his career. Arkoudas spoke with Tech at Bloomberg about this work:

Let’s start with a brief description of the book.

This is a textbook that teaches how to read and write proofs using a computer language. This combination of subject matter and programming tools is uncommon. There are many books on proofs out there, but their subject matter is either pure mathematics or pure logic. There are also books on proofs and logic specifically for computer science, but they are typically not supported by a computer language, so proofs are done using pencil and paper.

How is it particularly geared towards computer science students and professionals?

In two ways. First, most of the examples involve functions on fundamental inductive data types – such as lists, trees and dictionaries – and proofs about these functions. Inductive data types and recursive functions on them are the bread and butter of computer science. This book also studies some key programming language concepts, such as abstract syntax, operational semantics, and simple compilation techniques, and gives several proofs involving them. We also define and give machine-readable proofs of a number of things about some classic algorithms, such as Euclid’s algorithm and binary search.

Second, the proofs are written in a computer language called Athena and can be directly evaluated by a machine.

Athena is a programming language you developed.  What is it about Athena that made it suited to a book exploring proofs?

Athena is a blend of a higher-order functional programming language and a deduction language. This means you can not only write conventional functional programs in it, but also proofs that derive certain propositions. So you can have computation incorporated into proofs and you can have proofs inside more conventional computations. It is mainly this integration that makes the language an ideal vehicle for exploring proofs.

Why are proofs fundamental to the practice of computer science?

One can practice computer science and do it successfully without ever having to deal with proofs explicitly. But computer science practitioners need to reason all the time: about algorithms, code, distributed systems, security protocols, and so on. To reason about complicated systems correctly and fluently, it’s helpful – if not necessary – to be familiar with fundamental proof techniques, because these techniques capture the most expressive and sound reasoning idioms, patterns, and laws.

Why is this book notable for the current and next generation of computer science professionals?

Perhaps the most notable characteristic is that even beginner programmers can pick it up and start doing proofs on a computer within an hour.

This is the first mechanized proof system that combines programmability with true natural deduction. That’s a powerful combination. David Musser, my co-author, and I believe it can make proof methods accessible to a much wider audience.

Another distinctive aspect is its emphasis on generic proofs. The book develops a methodology for writing the most abstract proofs possible. These can then be reused simply by applying them to a different domain. This is somewhat similar to the idea of generic programming, which was developed by people like Alexander and David.

How do fundamental proofs play into what you do at Bloomberg today?

It’s not so much that I write detailed proofs of correctness, but that I can draw on these techniques to reason about the artifacts that I build. For example, one of the core parsing algorithms that I came up with is what appears to be an infinite loop of the form “while true, keep doing something.” Now, when you write a loop like that for a function that is expected to return a result, you better have some proof of termination sketched out.

For me, that was a fairly straightforward inductive argument. I don’t think I could have thought about it properly, let alone come up with the right argument, without a mastery of these fundamental techniques. There is no doubt in my mind that formal training in proof techniques can be very helpful in a computer science career – that’s certainly been the case in my career.