Code is Engineering; Types are Science
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 rules that help you attain your goals. These patterns of thinking have very 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, » Read More
Like to keep reading?
This article first appeared on tweag.io. If you'd like to keep reading, follow the white rabbit.