Correctness — the paradigm for sustainable software development

March 27, 2019 - Learning, Software - 18 minutes

Edit (2019-04-09): A quick qualifier for future readers. This post talks about correctness in the sense of correct code and not formal proofs or formal specifications. I refer to correctness in the sense of avoidable runtime errors.

In this post I want to explore some ideas that I’ve been working on over the last few months as I’ve studied and developed in more languages and paradigms.

What is a bug?

It’s a good question. Is it something that you missed? Is is undesirable behaviour because of an unintended side-effect? Is it scope creep that wasn’t accounted for? Was it a failure to understand the design for a given solution?

I think many of us would internally have a complex model of what constitutes a bug in our software. But let’s take the Wikipedia definition for now…

A software bug is an error, flaw, failure or fault in a computer program or system that causes it to produce an incorrect or unexpected result, or to behave in unintended ways.

However, there’s a temporal element that is missing here. “When” would you say that the software had a bug?

  • When it was found by a customer or client?
  • When your test suite picked up a syntax error?
  • When your compiler caught you passing an Integer instead of a String?
  • When you wrote out the model of your knowledge on paper?

Recognising a failure in your model of reality early on, is crucial to the development process, so that we can ensure our software is reliable and can do the automated task that it was designed for, and minimise the damage your broken model will apply to the world.

We are fortunate to live in a time where we have languages and tools that can help us recognise when our model is broken.

We’ve been asking the wrong questions

There’s no shortage of discussion about paradigms and languages. In fact you can clearly see a form of tribalism around each group if you read through some comments on Hacker News, Reddit, etc.

And from a social perspective, this makes sense, right? We’re all looking to be a part of communities and have that sense of belonging with the work that we do so that we can share it and benefit with others.

I was a musician in a former life, and these conversations about tools and languages are like the times when we would sit around and nerd out on music gear. What mouthpiece do you use? What’s your amp setup like? What strings do you prefer to use?

As you progress through your journey, you will realise that these are just tools. The real power comes from the intention of the musician and the values that they hold in their mind in order to communicate with their peers and their audience.

Software development is no different in this regard. We are attempting to express something about the world, in code, and the values that we hold are reflected in the “thing” that we create, which impacts our peers during collaboration, and the end users when it is shipped into production. These then go on to cause many other effects in the world of business, culture, etc.

Having arguments like, “object-oriented programming is dead”, or “functional programming is the way of the future”, is slightly missing the point. These tools and mindsets are backed by our values.

We need to first start at the fundamental core values that drive everything in order to gain understanding on the choices that we make.

An idea from the early years of software development

Let me start with a well-established fact: by and large the programming community displays a very ambivalent attitude towards the problem of program correctness. A major part of the average programmer’s activity is devoted to debugging, and from this observation we may conclude that the correctness of his programs —or should we say: their patent incorrectness?— is for him a matter of considerable concern. I claim that a programmer has only done a decent job when his program is flawless and not when his program is functioning properly only most of the time.

— E.W Dijkstra (Concern for Correctness as a Guiding Principle for Program Composition 1970)

This has been expressed in a few other ways by many folks in software. I won’t list them all (and I’d encourage you to seek these views out from your mentors) but here are two that hint at the same ideas.

Simple, correct, fast. In that order.

— Drew DeVault

Make it work, make it right, make it fast.

— Kent Beck

This is about the second part of this statement. How many of us make it past the first part of this statement during our daily work? If you did make it past the first part, can you honestly say to yourself that you made it right? How would you know if you did?

This is where the battle-lines need to be drawn in order to talk about language and tool selection. The tide is turning in the industry with software engineers actively working more with languages and tools that let us be correct before we unleash what we’ve written upon the world.

Developers — focusing on correctness. This is the paradigm shift that we are starting to see.

To say that it is just “functional programming”, or “object oriented programming” or <insert some other tool or technology here> is simply not true.

Perhaps in Haskell’s case, it’s the combination of pure, lazy and functional programming with parametric polymorphism is what gives the greatest strengths to the language to pursue correctness. I’d say Rust focuses heavily on correctness, but perhaps this is achieved by enforcing correct memory allocation/de-allocation along with having ADTs and pattern matching.

The thing you need to look at if you’re using say, a dynamic language, or object oriented design, is that in the long term, what is the language and mindset of “objects” with dynamic dispatch providing you apart from an endless stream of bugs that seem to keep reoccurring everytime you try an evolve the software to introduce a new requirement?

Correctness does not mean perfection

This is something that often comes up when discussing the idea of correctness. It’s something that I had associated together for a very long time myself. However I’ve come to realise something fundamental.

I know it might seem like a cliche, but there is no such thing as “perfect” software. How have I come to know this?

Software, is our knowledge, encoded so that a machine can perform actions based on that knowledge and so that other people can evolve that knowledge over time.

Our knowledge, is by no means “perfect”. The best that it can be is a representation of reality. One of the core ideas about correctness, is to put that knowledge under scrutiny, to see where the cracks start showing. Where does your model and understanding start to fall down? Is there a representation of your knowledge that means you don’t end up with unintended side-effects?

These “cracks” in your encoded knowledge are what I’ve come to know as failing invariants. An invariant is property of your program that holds true in all cases.


Do you know how deep the rabbit hole goes?

Here are some preliminary questions that can guide you and your team.

  • how many bugs a sprint do you have?
  • can they be classified?
  • how often do they occur / reoccur?
  • how much does your velocity drop when you have to implement a feature in a “legacy” part of the codebase?

When you start asking these kinds of questions, you might not know that there are other options available to you. But this is where I’d encourage you to start thinking about your tooling choices and your language choices.

As an industry, we spend an obscene amount of time maintaining software full of landmines. Why is this?

Partly for historical technical reasons, where maybe the practical implementations of correctness were falling short. Partly because our industry is very lucrative and we are essentially creating ongoing work for ourselves, every time we write code. Partly, and probably closer to home for many of us, is that the incentives in software development are misinterpreted and miscommunicated.

We are pushed by the needs of business to get things delivered, provide maximum value to users and customers and immediately jump to the next task, all with the intention of being profitable. I’m not against being profitable, in fact I’m all for it, but the direct focus on it can create a mindset that is counterproductive. Something like:

“I want to be able to get my software idea out into the world faster than anyone else, and be able to sacrifice edge cases and behaviour that would need to be considered in all non-successful path scenarios — I’ll fill those in later.”

The values of a weakly-typed dynamic programming languages seem to align with these ideas. I’m absolutely certain that this was never the intention of dynamic languages. They are extremely expressive in their ability to do meta-programming and the ideas behind Smalltalk and each behaviour in the system to be like a micro-organism talking with other micro-organisms via messages, is still something that hasn’t been fully realised.

However, the values of needing to “get stuff done, and quickly” or “move fast and break things” sound very much like, to some degree, they align with many businesses that operate in the world. This isn’t to say that it can’t be done. But it requires human discipline, communication and well functioning teams to achieve this to compensate for the shortfalls in this value alignment.

Can you blame developers? Can you blame businesses? Who are the culprits here in continuing to push this culture of poorly built software as an acceptable way of writing software?

We all are. We all are responsible for this as we go about our daily work. Which means we also have the power to change it for the better.

The road is long, until it’s not

I’m not gonna sugar-coat it — there are some very real barriers to taking the “correctness” road.

  • Functional programming and typed language theory is heavily academically influenced whilst the barrier to entry for programming has been lowered significantly.
  • Significant tooling and onboarding shortages for languages that are not popular “production ready” languages.
  • Success stories are few and far between, specifically the implementation details for others to learn from.
  • Industry fear — “Will I be able to use my skills elsewhere, are there jobs for Haskell developers, etc”
  • Missing buy-in from key business decision makers that correctness in automated systems, allows you to move faster in a sustainable manner, not slower.

I’m sure there are many more things that could be on this list, but I’d encourage you to not be tempted in using these points as excuses.

Every failed invariant costs something and is multiplied over time as these invariants overlap and happen to occur simultaneously. Time, revenue, customer engagement, happiness, employment retention, business sustainability, profits, team work, communication clarity. It really is a gradual boil until you are cooked. All of these things can be significantly reduced by many orders of magnitude.

There are huge benefits to traveling down the “correctness” path. What are some of the things we should be focusing on to get there? Here are a few that I think are important but by no means a definitive list.

  • Bridge the tooling gap for deploying software to production for languages that don’t have critical mass with conventions for deployments.
  • More story telling along with details of safe migration paths and deployment techniques for different technology stacks.
  • More accurate and accessible comparisons of learning OOP design patterns vs Functor, Applicative and Monad with relation to correctness - and specifically, how OOP is not equiped with the tools to acheive the correctness outcome at its core.
  • More communication from software teams to other teams in businesses about the benefits that they have received due to side-effects of correctness such as, increased developer happiness, positive learning culture, increased productivity and especially the financial gains.
  • Break the “not invented here” syndrome as individuals and as teams. Instead, stand on the shoulders of giants who dedicated enormous portions of their lives to finding principled, scientific, formal and provable approaches to developing correct software.

A final thought

The experience that many people have with learning Haskell, for example, is that they aren’t able to be productive right away. They aren’t able to write a program easily — which can be pretty demotivating if you are productive in your existing paradigm.

They then make the mistake of thinking that it must be that difficult to write all Haskell applications, forever. A continued cost. I also remember seeing colleagues struggle with Rust for similar reasons.

Just remember, the first time you try this — you are trying to learn a new way of thinking. That’s what a paradigm is. It doesn’t always come easily. But once you get it, you will only pay that cost once, and be able to reap the benefits from that mindset forever.

The industry is starting to make a lot of noise in this space with the likes of functional Scala, Typescript, Purescript, Elm, Haskell, Rust, Coq, Agda, Idris and many more. Some of these aren’t practical (yet) for writing production code but many of them are. I’d encourage you to spend time looking at the possibilities that exist on the spectrum of tools in the correctness paradigm.

We all have a finite amount of code that we can write in our lifetimes. Do we really want to be dealing with the same classes of (solved) problems until the end of your career whilst leaving a trail of un-maintainable software and unintended side-effects in your wake for your peers, businesses and the world to deal with?

We can do better. And as we do — let’s share the message of correctness with people who can leverage this idea outside of just the software community.

As always, I hope this is useful information to you and thanks for reading!

If you like this post and want to get in touch, please reach out and follow me on Twitter.