For almost as long as I’ve been programming, I’ve had a gut feeling that writing software should be easier. But I couldn’t name this feeling and didn’t understand it. I couldn’t describe it to others. So for a long time, this vague idea languished and remained as nothing more than a feeling.

Over the years, this feeling has grown into a calling. It’s something I have a hard time not thinking about or working on. Now that I’ve been done with my PhD for a while, I decided it was time to understand this idea and figure out exactly what it was that I wanted to work on.

This post is my attempt to transform that gut feeling into a coherent idea that I can explain to others: specifically, a “mission statement” for my career. There’s no better tool than writing for turning muddled thinking into crisply defined ideas, so that’s what I’m doing here.

Secondarily, I’m also writing this post in the hopes that other people might have tips to share on how to do this kind of work in industry, or pointers to topics I should look into.

My career mission is “to give software developers knowledge and tools to help them reason about their programs”. Read on if you’d like to know what I mean by this, why it’s where I want to focus my life’s work, and what I see as my next steps.

What This Mission Means

Let’s unpack some of the terms in that mission statement.

“Reason About”

First, what exactly do I mean by “reason about”? I mean that a programmer should be able to hold some model of their program in their head that helps them understand how the program works and predict what it will do. This is effectively what is known in science as “predictive power”.

To make this concrete, here are some examples of the kinds of things that help a programmer reason about their program in the above sense.

• Lexical scope: helps the programmer determine what variables are in scope with just a simple scan of the abstract syntax tree.
• Structured programming: enables the program to be subdivided hierarchically into “chunks”, so that the programmer can infer facts about individual chunks and then compose those facts into a single fact about the larger whole (i.e. it enables “compositional reasoning” about program chunks).
• Static type systems (especially sound ones): automatically check the programmer’s intent against what they wrote, ensuring that certain kinds of errors can never happen at run time.
• Rust’s borrowing system: prevents certain classes of errors not caught by traditional type systems, like use-after-free and data races (with the exception of code marked with “unsafe”).
• Abstraction and information hiding: enable the programmer to predict how some chunk of code interacts with the rest of the program by reasoning only about that chunk’s interface and specification, rather than its entire implementation.
• Proof assistants: automate some of the deductive reasoning about programs to help the programmer prove certain theorems about their programs. The theorems might be freedom from a certain kind of error, or a guarantee that the program implements a specification, or anything else the proof assistant’s logic supports.

Conversely, here are some examples of tools and practices that a programmer might use to gain confidence in their program, but don’t enable the kind of reasoning I want to work on.

• Testing (e.g. unit tests, integration tests, load tests, etc.): tells the programmer whether the program has some desired behavior, but only after executing it. An over-reliance on testing leads to a kind of guess-and-check style of programming, where the programmer writes some code without understanding it, then just runs the test to see what happens. (I’ll talk more below about why I think this is a bad idea.) You see this most often with students just learning to program, but occasionally in professional programmers, too.
• Runtime verification: checks for certain error conditions while the program is running, but by the definition of “runtime” it can’t predict what will happen.
• Model checking: predicts whether the program will obey some specification (e.g. the program will never deadlock), but doesn’t necessarily help the programmer understand why that’s the case. If the only possible results from running a model checker are just “yes” or “no” (or “unable to determine”), then relatively little information is gained. In this sense, model checking is similar to testing in terms of the reasoning ability it provides: it can say something is wrong in the program, but it can’t say where the problem is. (Some model checkers provide concrete counterexamples in the “no” case, which might change how I categorize them.)

These examples and counterexamples are separated mostly along static/dynamic lines, but model checking is an exception to this rule. It’s generally considered a static technique, but it doesn’t increase a programmer’s understanding of their program in the way I’m looking for. It might be that what I’m looking for is really static, compositional reasoning, but I need to think through some more examples before I’m convinced that that’s true.

“Knowledge and Tools”

Now that we’ve covered what I mean by “reason about”, let’s talk about the “knowledge and tools” aspect of this mission statement. I wanted to explicitly call those out as distinct concerns because while we know that tools can help a programmer reason about their program, it’s equally important to know that their ability to reason about their program is also determined by how they design and write their program. Some program structures are much easier to reason about than others (consider spaghetti code versus a well-structured program), and some tools work only if the program is written in a certain way. Programmers need to know how the design of a program affects reasoning ability, and that can’t come (exclusively) from a tool: programmers have to know this from the start and use this knowledge while creating their programs.

Concretely for me, listing both “knowledge” and “tools” in my mission statement reminds me that this mission involves not just tool-building, but a certain amount of teaching as well.

Why This Particular Mission?

Software developers need to reason about their programs in order to do any kind of meaningful work. While it’s sometimes possible to write code that “works” without really understanding it (e.g. with the “guess-and-check” approach mentioned in the above bullet about testing), that’s usually a bad idea. Here’s why:

• Test cases can tell you that your program works for those specific cases, but without a predictive model, you can’t be sure that the program will do the right thing in all cases.
• If you ever need to modify your program, you’ll have no idea what should be modified unless you understand how it works.
• When something goes wrong in production (as it inevitably will), you’ll need to understand how the program is supposed to work if you want to have any hope of finding the root cause of the issue.

By default, we try to do this kind of reasoning in our heads. For the really tough problems, we might break out the pencil and paper. That’s how it happened historically, and that’s how most of us do it when starting out today.

But as Fred Brooks wrote in No Silver Bullet in 1987, “software entities are more complex for their size than perhaps any other human construct.” Douglas Crockford made a similar observation in JavaScript: The Good Parts in 2008, saying “computer programs are the most complex things that humans make.” And not only that: programs are getting more complex every year, with the shift from single-machine to distributed programs, programs that have to run on heterogeneous platforms (desktop computer, mobile phone, smart TV), and other advances in modern software.

Human reasoning alone can’t keep up with this rise in complexity. Some people are able to hold more information in their head than others, but we all hit our limit at a certain point. Software complexity will only continue to surpass the ability of the human mind to reason about it.

Computers, on the other hand, are designed precisely for these kinds of heavy-but-mechanical symbol-processing tasks. Even a run-of-the-mill laptop today is orders of magnitude faster and less error-prone at this kind of work than the best human reasoner. We need computers to automate some of this work for us if we want to have any hope of continuing to reason about modern-day software.

The good news is that there is a lot of untapped potential in this space. The last couple of decades have seen a number of advances from formal-methods/programming-language/software-engineering research trickle down into industry, like SAT-solver-based verification and more advanced type systems such as the ones in Rust and Haskell. Other techniques like dependent type systems appear to be becoming more usable, and there seems to be a growing interest in this kind of work from software developers. I expect this trend to continue.

My hope is that in some future year, a programmer will be able to sit down at their desk and write a program in concert with a kind of uber proof assistant. The programmer would set goals and guide the overall direction of the work, while the proof assistant would take care of the mechanical reasoning tasks and answer the programmer’s questions about their code. By offloading the heavy burden of reasoning over to the computer, the programmer’s brain would be free to take on the more creative and intuitive tasks. Thus the human and the machine would complement each other’s skills, leading to an end result that neither could have achieved on their own. I’m heavily inspired in this by J. C. R. Licklider’s Man-Computer Symbiosis and Thomas A. Limoncelli’s Automation Should Be Like Iron Man, Not Ultron.

What Are My Next Steps?

Even with the specific definitions used above, my mission statement is still pretty broad. That’s intentional: I’m trying to identify the kind of work I want to do and think would be valuable to the world, but be able to adapt that purpose to different environments and contexts depending on where I am in my career.

That said, there are a number of general concepts in this area that would be good to know regardless of the specific project I’m working on. Here are a few things I plan to do in the short-ish term:

• Finish reading The Little Typer and do the exercises, as a way to learn the basics of dependent types.
• Read (or at least skim) Ringer et al.’s recent survey of proof engineering, QED at Large.
• Learn about compositional reasoning in general, and specifically how to design programs that are amenable to it. I’m sure there’s a ton of work in this area, but I’m hopeful there are some common/fundamental ideas I should know about (suggestions?).
• Maybe experiment with a theorem prover like Coq or Agda, since I don’t actually have that experience yet. I’ve heard that Software Foundations and Programming Language Foundations in Agda are both good places to start.

Finally, I’d also like to figure out how to do this kind of work in industry. Academia wasn’t a good environmental fit for me, and I prefer to build useful tools that get into developers’ hands quickly rather than seek out fundamental truths that can take a long time to find their way into practice. But much of my mission sounds more like a classical research program than an industry project, so I’m still figuring out how to actually do this work outside of the typical academic setting. Perhaps there’s room for a kind of tech-transfer role in this area, but I don’t know what that looks like yet or how to make it happen. (Note that I intend to stay at Google for the time being, but who knows what could happen in the longer term?)

Do you have suggestions for additional topics I should learn about? Ideas on how to do this kind of work in an industry setting? Let me know! I’m @SchuCodes on Twitter (I’ll start a thread about this post), or you can just email me at jonathan.p.schuster@gmail.com. Thanks!