# Code is Engineering, Types are Science

379 Programming is a diverse activity that requires reasoning in many different
ways. Sometimes one has to think like an engineer—find the best solution for
a problem under multiple constraints. Other times, one has to think like a
scientist—observe the data points you have in order to establish general
different natures.

In this blog post, I will explain these patterns through the theory of
reasoning of Charles Sanders Peirce. Peirce divides reasoning into
three complementary processes: deduction, abduction and
induction. In the following sections we will go through these logical
processes and see how they relate to software.

But before starting, I want to make explicit the underlying subject of this
post: plausible reasoning. Plausible reasoning does not imply
certainty or truth—it better reflects the concept of an educated guess. At
minimum, these guesses must not be contradicted by the information we have
at hand. At best, with more information, we can choose the guess with the most
chance of being true. With that out of the way, let’s dive into our
definitions.

## Deduction

Deduction is the process of reasoning that we acknowledge the most. It is what
we learn in mathematics, and also what we think about when talking about logic.
The basic schema is the following: if we know a fact `A`, and we know that `A`
implies `B`, then we know the fact `B` (modus ponens). We will represent this
process with the following diagram:

In philosophy books, it is very common to identify the sides of this triangle
with the following phrases:

• Socrates is human (left).
• Every human is mortal (right).
• Therefore Socrates is mortal (bottom).

which can be useful when trying to identify the reasoning patterns we will see
next.

The practical utility of deduction is that it is able to reduce the scope of a
problem: if we want to achieve `B`, and we know that `A` implies `B`, we can
change our goal to `A` if we think that is useful.

One particularity of deduction is that the result of a deduction is the
certainty of a fact: if we achieve `A`, we are certain to achieve `B`. As we
will see, this is not the case for the other reasoning processes.

In Haskell programming, for example, deduction is omnipresent. Every time you
apply a function of type `a -> b` to a value of type `a` in order to produce a
value of type `b`, you apply deductive reasoning.

## Abduction

A client sends you a bug report describing some anomalous behavior in the
software you work on. You run it locally, and observe the same behavior. After
some changes in the code you do not observe the offending behavior anymore, and
declare the bug as solved.

The first thing to notice is that the reasoning above is not logically correct.
Indeed, we can simplify it as follows:

• I don’t see the behavior anymore.
• If the bug is solved, I should not see the behavior.
• Therefore, I solved the bug.

It is possible that the anomalous behavior was the result of two interacting
parts, and your manipulation of one of them made the underlying cause of the
bug, present in the other component, not visible anymore. However this is
plausible reasoning—given the constraints you have (the observation or not of
bugs locally), you managed to propose a solution that is coherent,
non-contradicting, that has a chance of being correct. And as developers, we
know that very often, this works.

The mechanism of abduction is the following: if we know a fact `B`, and we know
that `A` implies `B`, then we abduce `A` as a plausible thing. This can be
represented in the following diagram:

Abduction is the process that we identify with writing code and engineering,
since it is about solving a problem under constraints. This is not the only
component of engineering, but it is one of its defining aspects. In the case of
the diagram above, for example, the constraint is knowing that `A` implies `B`.

We can now connect abduction with writing code in a typed language. What
happens when we try to make an action plan based on abductive reasoning? If
we take `A` to correspond to “code works” and `B` to correspond to “code
typechecks”, we can act using abduction as follows:

• I want to write working code.
• My only information is that working code must typecheck.
• Therefore, I try to write code that typechecks so that it can work.

This reasoning can be successful or unsuccessful depending on the context. It
has almost no chance of working in the C language, but has a very good chance
of working if you doing something simple in Idris. It can also describe the
experience of a beginner in a Haskell codebase, and the expression “just follow
the types”. This will not necessarily lead to working code, but will allow the

In summary, abduction corresponds to using all the information one has in order
to obtain a reasonable, or if the context permits, the best solution to a
problem. This is typically the job of the engineer, and something that any
programmer can relate to: do the best you can under the constraints you have.

## Induction

Your company’s server crashed at a given time last night. You read the log
files and see that there is an “out of memory” error timestamped to the moment
of the server crash. Therefore, you diagnose this error as the culprit for the
server crash.

The first thing to notice is that the reasoning above is not logically correct.
Indeed, we can simplify it as follows:

• The out of memory error happened at time T.
• The server crashed at time T.
• Therefore, the out of memory error caused the server to crash.

Indeed, it can be that case that this error was safely caught and the server
crashed because of an electricity problem. However this is plausible
reasoning — given two facts that have the same origin (the same moment in
time), you managed to establish a causality that is coherent,
non-contradicting, that has a chance of being correct. And as developers, we
know that very often, this works.

The mechanism of induction is the following: if we know a fact `B` and we know
a fact `A`, then we induce `A` implies `B` as a plausible thing. This can be
represented in the following diagram:

Induction is the process that we identify with writing types and science,
especially with natural sciences, because it is about establishing
constraints and general rules that limit possible behaviors. This is not
the only component of science, but it is one of its defining aspects. In the
case of the diagram above, for example, the constraint is the established
constraint is that `A` implies `B`.

We can now connect induction with writing types for a library. What happens
when we try to make an action plan based on inductive reasoning? If we take
`A` to correspond to “code is wrong” and `B` to correspond to “code does not
typecheck”, we can act using induction as follows:

• I know some code is wrong, and I want to avoid it in production.
• Code that doesn’t typecheck doesn’t run.
• Therefore, I write types so that this code does not typecheck.

This corresponds to the post-hoc type modelling of an existing codebase, that
tries to preserve important invariants and prevent future errors. The
establishment of a type system is akin to the creation of a general rule that
allows some desirable code examples to be valid, and undesirable ones to not
exist.

In summary, induction corresponds to establishing an environment of constraints
and rules so that others, while working under these conditions, produce the
outcomes that are expected. This is typically the job of managers, and present
in many other activities, like teaching and parenting. This is also one of the
roles of scientific theories, to constrain the space of possibilities when
developing an engineering project.

## Conclusion

Here’s the takeaway:

• Even the most well-informed decisions we take are not logical conclusions of
facts – they are most often just plausible theories. At minimum, they must
not be false, but if possible, we must use the information we have at hand to
make the best decision.

• Abduction and induction are simple mechanisms yet omnipresent. Being able to
identify whether we are using one of them makes it easier to know how to find
the weak points and to better justify our arguments. Abductions and
inductions always require arguments.

• Being able to identify where plausible reasoning was used in some decision
process can show where possible errors can happen, or where new data can show
problems that were not foreseen before.

In another note, what about writing tests? This is also an inductive activity
like writing types, they only differ in breadth and power—while types can be
imposed not only to developers, but also to users of a library, tests can
impose constraints that are unavailable to a type system.

Globally, the message is that programming involves activities of different
natures. Sometimes you are just plumbing functions together and you have to
think like a mathematician. Sometimes you are writing functions and have to
work under constraints and think like an engineer. And sometimes you have to
establish frameworks and give appropriate constraints to yourself and your
coworkers, work with the evidence you have and think like a scientist. And no
part in this game is more or less important than the others. They are
different, yet complementary.