Let me begin with a small observation,
and if you are involved in the data profession, you are painfully aware of this:
Scenario: You ask about the data quality and someone shows you a series of tests, monitoring dashboards, and metrics that are supposed to prove that everything works as it should.
Here’s the problem: testing, at best, can reveal the presence of errors, it can never show their absence. Dijkstra warned against this years ago, and this same intellectual shortcut has grown tremendously in the data profession. Especially where anything close to a formal proof is hard, and sometimes impossible.
Today, we build data pipelines and machine learning models in an ad hoc experimental way. We add some garnish (infrastructure as code, basic tests and checks) and ship them to production. Detection is cheaper and more convenient than prevention, and whenever we are given the choice and are under a hard deadline, it is easy to prioritise the instruments and skip the discipline. This is not an argument against testing but rather where it belongs.
What we are really lacking is a disciplined way to prevent errors from happening in the first place: a way of making certain errors impossible by design.
Ignoring this is similar to ignoring gravity when designing an airplane.
This series is an attempt at such a discipline, to bring back the engineering in data engineering, the science in data science, and to show that data systems can be made with a prevention-first approach.
What I propose here is an approach that aims to ensure a data system is correct by design. This is part one of the series:
This part explains the main principles.
The second part gives a step by step recipe to follow.
Finally, the last part will focus more on: formal arguments to prove what we are building is correct.
I expect many people will disagree with this. Your comments and challenging arguments are welcome.
The why and how of correctness by design
If you are not convinced this problem is big enough, meditate on this quote:
“As long as there were no machines, programming was no problem at all;
when we had a few weak computers, programming became a mild problem,
and now we have gigantic computers,
programming has become an equally gigantic problem” The Humble Programmer, E. W. Dijkstra (1972)
Today this is orders of magnitude larger, and I suspect it is a matter of a few years (if not a few months) before this gets completely out of hand.
About seventeen years ago, when I took my first machine learning course, one of the notes I took reads something along the lines of: “deep learning is currently of little practical use, perhaps it may be useful in the future”. I mention this not to display my poor judgement, which speaks for itself, but as a reminder of the speed at which this field has grown. Problems that, back then, were not even considered possible to solve are today expected to reach production in one or two months. There is a gap that is growing even faster now with how we use language models to write code.
Our capacity to build has grown dramatically, our capacity to understand what we build has stayed about the same.
That is why we need a prevention-first discipline. The aim is not to guarantee every module is correct. It is to avoid as many errors as possible by construction.
The framework I will suggest here has three steps: 1 Prove → 2 Check → 3 Monitor
Skipping any step in this ladder is a choice that should be explicitly made rather than being implicit.
But before we explain this, it makes no sense to talk about “proving a system is correct” unless we define what it means for such a system to be “correct” in the first place.
So all of the steps above depend on having a proper definition. How can we define what correctness means for a data system?
First, what does “correct” mean
There is no reason to prove a system is correct if you cannot define what correct means. This section is about defining what the system does in a way that is falsifiable.
Most projects have a generalised statement of what they should achieve: “Make our data more up to date”, “Improve the data quality of X” or “Make our data products discoverable”. The issue with these generalised statements is that there is no way of ensuring we really achieved them other than a subjective feeling.
Just like saying “Cleanse the energy of the data” these generalised statements mean different things to different people. And, when we claim to have achieved the goal, what it meant for the person requesting it may be very different from what we have built. A falsifiable statement instead is clearly defined and avoids this problem. For example: at least 99% of daily datasets are available by 07:00, compared with the current 92%, for 8 consecutive weeks. Those proficient in the data jargon will state that this is just an SLO (service level objective), it does overlap with it but the goal here is to use this statement as the base that everything else is derived from.
One way to define this is to think about:
What is measured
What is the current state (the baseline we’re comparing with)
What is a measurable improvement (for the project to be called a success)
Time periods: how long until we know the measurable improvement
Important constraints and limitations
We don’t always need all five, the main thing we need is for the statement to be, you guessed it, “falsifiable”. This gives us a clear definition of what it means for what we built to be “correct”.
Most of the time, teams resist writing such falsifiable statements because of two reasons. The first is that they don’t have time: this usually means that delivering fast is more important than delivering the right thing. Sometimes that trade-off is worth it. But it should just be clear that it is a choice, made explicitly and not just happening by default.
The second is that the problem is hard to understand and it is unclear what to measure: this just means the problem is not understood well enough, which only means the experimentation step is not finished.
You don’t need a falsifiable statement at the start. Often, you need to experiment with ad hoc code before you actually understand the problem, to go back and forth with the people involved. This step usually helps you get a true understanding of what the problem requires, how it can be solved and what can be measured. The experimentation step is necessary, because it helps us understand what is involved in the problem. The experimentation should not be restrictive, which means it allows for the kind of creativity that is needed to solve certain problems.
Sometimes measuring is hard, other times impossible, and for a few problems it can be misleading. And when a measure becomes the target, it ceases to be a good measure (Goodhart’s law, in Marilyn Strathern’s phrasing). None of it is a reason to skip the definition step. Because at the end of the day you will be making either implicit or explicit measures. It’s the choice between defining, and going with the vibe.
In summary,
Whether you like it or not, you are making a hypothesis. So make sure it is clear and explicit, and define your project’s goal as a falsifiable statement.
The prevention-first discipline: prove, check, monitor
Testing and monitoring are necessary. But given that these can only ever demonstrate the presence of errors, the better question is how can we make some errors structurally impossible before we even write code?
I will argue that we need to take a more formal approach: to borrow, as far as is practical, from formal mathematical reasoning. Explicit reasoning about correctness has been almost entirely absent from mainstream data engineering (despite the fact that this field rests on formal foundations such as relational algebra and type systems). Adjacent fields like compilers, databases, and distributed systems treat formal reasoning as a first-class tool. But data and machine learning pipelines largely don’t.
There are however a few reasonable objections to this. The first is that Data and ML pipelines cannot be fully proven, some parts depend on things we don’t control: upstream sources, the stochastic nature of models, data/concept shifts and drifts to name a few. And the second is that a proof is just as good as the assumptions we make at the start. And the assumptions we make in the data field are bound to change.
So I am not proposing we formally prove the entirety of a pipeline, what I’m suggesting here is a middle way.
This middle way looks at correctness as a ladder, where we are clear about which tradeoffs we are making when we skip an important step. As we’ve defined it above, this 3-step ladder depends on the problem at hand. And once again, skipping any one step in this ladder is a choice that should be explicitly made rather than being implicit:
Prove what is provable → Check at every boundary → Monitor the rest
Step 1 - Prove what is provable
A proof is an argument that a statement is true for every possible input (not just the inputs you tried). The next article here describes what to prove and how to prove it, for now let’s just define what we mean by “prove”.
In slightly more formal words:
Given a system defined by a function f, that accepts a defined set of inputs I
- under a defined precondition P over its inputs,
- and a postcondition Q over the input/output pairs.
Proving is establishing that∀ x ∈ I; P(x) => Q(x, f(x))
In other words, that for every possible input, if the precondition is satisfied by the input, the postcondition is satisfied (by the input/output pair).
Testing instead of proving is equivalent to checking Q(xi, f(xi)) is true for a finite set of chosen inputs xi that satisfy P.
The formal method crowd will recognise Hoare’s triple here, but the goal is not to get too formal. Of all the steps, this one invites the most criticism. Engineers will usually argue that proving would take too long, whereas mathematicians and theorists will usually argue that proving is worth the tradeoff. The reason we’re taking a middle way here is that we do not want to tradeoff time either.
Let me just explain the reasoning here:
We have to see this as a spectrum that goes from informal types of reasoning (like an intuitive explanation in a markdown documentation) to the more rigorous formal methods (such as using machine checkable proofs).
And the good news, in my experience, is that the cheaper methods find most of the errors, in other words: just spending time reasoning about the problem and writing an informal argument usually catches the majority of potential errors. Writing down in plain words why a job should be deterministic is often enough to find out it isn’t.
In between those ends, we find types that make invalid states unrepresentable, arguments by induction over partitions etc. (more details in the next article).
If we breakdown the system we are building into multiple components. We want anyone reading the design to see where every component is and why it is there.
In the next article, I will go into details about:
What properties you should prove (such as idempotence, determinism etc.).
What arguments you can use for different scenarios.
Where testing fits here: tests can help us make the argument stay more up to date with the implementation. The proof holds for the design, but the code may still drift from it. Property-based testing comes handy here, with libraries such as Hypothesis in Python. The property under test is the proof’s own statement: if P(x), then Q(x, f(x)), run on thousands of generated inputs that satisfy P. The test still only samples, but it samples something different: not the world, but whether the code faithfully follows an argument that already covers every input.
In summary,
Before writing code, and before writing tests, we should try to argue for the most important properties, the recipe in the next post gives an example of this, followed by the final post that goes into more details on using formal arguments.
Step 2 - Check at every boundary
None of the proving we did earlier ensures that the input satisfies the precondition. That is where checking comes. The moment an input reaches our system, we must check that it satisfies the preconditions we depend on, otherwise we reject it.
A boundary here is anywhere data is handed over: where it arrives from an upstream source we don’t own, where it passes from one module to another, where it is written to a table other people read, where it is fed to a model, served to a user etc.
A check is not a test: the two are easy to confuse. A test runs before deployment, on inputs we chose. A check runs in the deployment environment, and includes real inputs. A test asks: does my code behave on the examples I can think of? A test samples the domain. A check attempts to guard this domain instead.
This is in line with designing by contract,
a concept introduced by Bertrand Meyer in the mid-eighties. The current work on data contracts (popularised by Andrew Jones and Chad Sanderson) applies this idea to data, and is very useful. But a contract should say much more. A contract that says “quantity is an integer” is a very weak contract, it’s a simple type declaration.
A contract in Meyer’s terms binds two parties: the supplier guarantees the postcondition only if the client satisfies the precondition. A data system thus acts as a client of the upstream sources, and a supplier for the downstream users of the system. And as such it needs to define the contracts at both boundaries.
A useful contract has to define:
Structure: fields, types, nullability, keys.
Meaning: ranges, units, allowed values, uniqueness, and the relationships between fields and between tables (for example: every order refers to a customer that exists, a refund never exceeds the original payment).
Delivery: when the data should arrive, how much of it we expect, and how complete it should be.
All the above should be applied to: the preconditions (write guarantees: rules that a data producer or client must satisfy before writing/streaming),
the postconditions (read guarantees: promises a data system or processing function makes upon completing a query or transformation, e.g., output dataset row counts match expected aggregates, null-free columns),
and the invariants (think here about the consistency of storage and states: rules at the level of the system itself, that must always remain true at rest or between mutations, these are things such as foreign key integrity, partition balance, chronological event ordering etc.)
Two principles complete the checking step:
Parse don’t validate: popularised by Alexis King in her blog post “parse, don’t validate” is about ensuring we cannot represent invalid states through parsing. Once parsed, the precondition is satisfied.
Reject rather than repair: as much as you can, if a check fails, reject the record. Fixing silently may end up hiding errors.
In summary,
A proof is only as good as its preconditions, a check ensures those preconditions hold in practice. Check every boundary, reject rather than repair (not always but as much as possible), parse don’t validate.
Step 3 - Monitor what is outside of your control
Some things will be outside of your control. Data drift, sources that change meaning with no notification, the stochastic nature of ML components whose behaviour is best described by black magic etc.
The proofs and checks rest on assumptions. Monitoring is simply about watching those assumptions. My criticism of monitoring is only because a lot of the time we make it the whole strategy. If you have gone through the previous steps, then you know by now what to monitor and alert for.
Monitoring what you cannot prevent is a necessity.
Monitoring what you could prevent is laziness, manifested as a dashboard.
On ownership in monitoring: monitoring and alerting should always have clear ownership. We have to be clear on who will take action, when they must take action and how they will know (for example: an alert email or so, or if they routinely check a dashboard every Tuesday morning), and what the action is. Setting a dashboard that nobody looks at is as good as doing nothing.
Working backwards from monitoring: when we find issues through monitoring, it is the opportunity to add checks and to revise the architecture/design of the system.
In summary,
Derive what you must monitor from your assumptions. Give every monitoring modality or alert an owner, and treat every recurring alert as an invitation to move that error back up the ladder, to prevent it from happening in the first place.
None of this is new
Nothing in this series is new. If anything, this argument has existed for decades, but the data professions seem to ignore most of this work. Proofs, contracts and checks are decades old.
So why has the data and machine learning world not taken them in (for the most part)? Not because they don’t apply, but because we are able to get away without them, until the day we’re not. Data errors rarely crash, they rather mislead, quietly. And when they do crash they create a new problem that we build another system to solve. But perhaps also because the data and machine learning fields have a lot of stochastic components built in that we use as an excuse. Add to that the speed at which we’re trying to build things today to “keep up”. That is exactly why we need the discipline more, not less. The theory is there, and so are the tools. What is missing is the habit.
I am in no way claiming:
That every data pipeline should be formally proven.
That tests and monitoring are useless. They are just not preventive, and proofs do not replace them.
That this is faster. It costs some more design time up front. Which I believe is much cheaper in the long term, but I have no study to prove it. So do see this as a hypothesis, and if you have any evidence in either direction, I would love to hear from you.
In the next article we will go through a more detailed step by step recipe for building data systems that prevent errors, using a worked example.