This post was inspired by a talk by Adam Chlipala. Indeed, none of the ideas presented here are original ideas — check out a talk he gave for a more polished/less watered-down presentation of these ideas.

Most software nowadays is a blend of implementation and specification. What do I mean by that? First, let’s go through some definitions.

1. Specification is how we want our software to run.
2. Implementation is a set of directions stating how the software will execute
3. Verification is checking that the implementation satisfies the specification

Formal vs. Informal

1. Informal: in our heads, in our words, not rigorous, ideally precise, but captures the essence of the goal, not executable but usually not buggy (because presumably our goal is simple enough to easily reason about whether we indeed want it as a goal), and we can break it down into whatever granularity we want
2. Formal: rigorous, via some precise, exact language. Usually written in code.

Formal vs. informal specifications

1. Informal specifications: design doc, software spec docs, RFCs, uses english, a document
2. Formal specifications: software, yaml, infrastructure as code, business logic, machine learning code, a lot of functional programming code.

Now, back to the original claim: all software is a blend of implementation and specification. Surely, as we defined it, all software is implementation. So why would it contain both specification and implementation?

Let’s go through a simple example. Suppose we wanted to write software that computed the factorial function. We can formally define the factorial function as follows: f(x) = x * f(x-1) if x > 1 else 1. Alternatively, we could define it as f(x) = prod_1_x(i). Indeed, both definitions are equivalent, and that could be shown using a simple proof by induction.

Now, suppose we wanted to write software that computed the factorial function - aha, we’ve already done that! Since we required the defintion to be written in formal terms, it’s essentially executable. We could merely use either of the two definitions and write those in software to get our factorial function.

Here’s where it gets a little tricky. What is the specification, and what is the implementation? The specification is how we want our software to run, which is to execute the factorial function as defined by f(x) = prod_1_x(i) (as an example, if we were to pick that definition of the factorial function as our specification). The implementation, is how the software actually runs. If we were to run the definition as the function, then the implementation would be f(x) = prod_1_x(i). Which exactly matches the specification.

Now suppose our implementation opted for the recursive implementation, whereas we were to keep the specification as prod_1_x(i). In order to prove that our implementation satisfies the prod definition/specification, we need a simple proof by induction. That proof would be the verification process. In this case, the specification and the implementation aren’t exactly the same, so we need an extra step (verification) in order to guarantee that the implementation does indeed match the specification. (Note that if they were the same, the verification step would be a trivial proof that f(x) = f(x)).

Modern software as a mix of implementation and specification

I arrive to my original point. All of software is a mix of specification and implementation. Consider a function that returns the amount to charge for a service based on a user’s age. function service_charge(user_age) = 10 if user_age >= 18 else 15. This surely reflects the business logic, i.e. the specification. Yet this function might be hidden in a codebase containing a lot more business logic along with implementation details (read an http request, parse the header and contents, connect to the database, pull the user’s age information, calculate the service charge, call an API to make the charge, write the transaction to the database, etc).

Potential source of bugs

In the real world, we don’t always have the luxury of verification. Many times, we don’t even have the luxury of a formal specification. Whenever the desired specification doesn’t match the implementation, we consider that an error in the implementation, also known as a bug. Of course, the bug may come at any point in the process of converting desired specifications to implementation.

1. Errors in the informal specification: what we want may differ from what we write in a document about what we want
2. Errors in the formal specification: what we specify as code as desired behavior might not match our written specification
3. Errors in the implementation: the implementation might not match the specification, whether formal or informal.

Formal specification vs. unit tests

A quick sidebar on testing. Often the specifications aren’t written out in the form of some formal specification, rather as a set of tests that can execute the implementation and check some property of it. These tests, unless they perform some kind of static code analysis, have an example input to the software and check a desired output. I would argue that this is a kind of formal specification, albeit an incomplete specification as it only describes how we want the code to behave for a single example (or set of examples). While they suffice for some cases, they by no means offer a complete specification of behavior of software, and indeed many bugs aren’t caught by unit tests because they are incomplete.

What I wish software engineering looked like

Simply put, I wish software engineering looked like this:

1. Software engineers determine the informal specification for the system, i.e. the desired behavior of the system
2. Software engineers formalize the specification in code
3. The compiler/computer/software whatever, executes the specification
4. The software engineers write unit tests or an extra set of specifications to debug the formal specification, as a sanity check that the formal specification matches the informal specification

In other words, I wish that the third type of bug, errors in the implementation, didn’t exist, and we could focus entirely on the core logic of the system.

Every software engineer has a list of properties that they believe to be true about the system. A mental model, if you will. And when they reason about the software, they use those properties to get a better sense of how the system operates. These properties can be defined in code, and we can automate reasoning about the system to make sure that the system satisfies the specification.

Why doesn’t this exist yet

Two main problems with this approach: 1) sometimes, you can’t execute the specification. Consider the specification for a sorting algorithm. f(x) = y where y = sorted(x). Sorted == all the same items AND each item <= next item. You can’t execute that specification because it offers no way instructions on how to get from x to y, it only states the desired relationship between x and y. 2) Easy tooling doesn’t exist. By and large, a lot of what we’re talking about boils down to functional programming. When it comes time to write formal specification, it looks very much like functional programming. We can write the specification in some functional programming language, and then execute it via the functional programming language.

How do we get there

The solution is a matter of defining new abstractions/interfaces to allow for faster software development by abstracting away the tedious, non-specification parts of software.

This all might seem trivial, but consider how much software engineering work you’ve done that is very trivial conceptually. Then consider writing out the work formally in its simplest form. Then imagine if you could immediately execute that formal definition. That’s what I want software engineering to be. That’s what I want it to look like. Ideally, there would be one system that handled all the innards, an operating system if you will, and all you would need to do is submit code to the operating system. Given how the world of software has evolved, can we make a new operating system that does this? That takes into account cloud/no cloud, the internet, distributed systems, gpus, etc.

The ultimate goal is to close the gap between idea and implementation — ideally, the implementation should immediately follow the idea, once the idea has been formally defined.

Sure, the amount of specification/implementation varies for each software engineer. When I worked with machine learning, it was mostly specification work, and most of my bugs were bugs in the specification (i.e. algorithm bugs or ml code bugs). So this doesn’t apply to everything.