Beyond Test-Driven Development

What is the purpose of software testing? What you’ll most likely hear from developers is that the purpose of software testing is to ensure a program does what it is meant to do. So, for those few (ha, ha) software programs that have bugs, is this because they don’t have adequate or enough testing? Some years ago Edsger W. Dijkstra¹ had something to say about this:

A common approach to get a program correct is called “debugging” and when the most patent bugs have been found and removed one tries to raise the confidence level further by subjecting the program to numerous test cases. From the failures around us we can derive ample evidence that this approach is inadequate.

Clearly Dijkstra did not buy into the test-for-quality approach (one that continues mostly unchanged to this day). Why would testing be inadequate? Because

[…] program testing can be used very effectively to show the presence of bugs but never to show their absence.

So what can be done? What alternatives do we have?

Formal methods provide different mechanisms to ensure program correctness, but their application is not always practical or even feasible, depending on the kind of software system. So Dijkstra, any other, more mundane ideas?

[…] instead of looking for more elaborate debugging aids, I would rather try to identify and remove the more productive bug-generators!

It sounds like you’re suggesting that, instead of testing the quality of the software, we should focus on improving it by removing bug-generators to begin with (whatever these may be). That makes sense. It reminds me of W. E. Deming (paraphrasing): You cannot test quality into the software; rather, quality needs to be built into it. So how can we identify, remove and, even better, prevent these “more productive bug-generators”?

Type-driven development is one approach, and the one I want to introduce here. In essence, it focuses on encoding the domain (as much as it is practically possible) in the type system and making types the point of departure for the rest of the development work. But before we go there let’s briefly look at the more popular (and surprisingly controversial) test-driven development (or TDD for short), and note their similarities and differences.

Test-Driven Development

Test-driven development, popularized by Kent Beck, is a software development methodology that emphasizes writing tests before writing the implementation. It follows a cyclical process that typically consists of three main steps:

1. Write a failing test: Developers start by writing test cases that define the expected behavior of a particular piece of code. At this point, the code to be tested does not exist, so the test will fail.
2. Write the minimum implementation that passes the test: Developers then write the minimum amount of code necessary to make the failing test pass.
3. Refactor and repeat: Once the test passes, developers may refactor the code to improve it in some way (e.g., its design, maintainability, performance) while ensuring the test continues to pass.

Some might argue that it makes no difference to write the test before or after the implementation is complete, after all, either way we test the same code… or do we? As Matthijs Thoolen points out “TDD is not about testing, it is about design”:

When practicing TDD we write code (in a test) to drive the implementation. […] By thinking about the design before any actual implementation has been written, we’re already making choices about the most important part of our code, the model. We have the opportunity to focus first on the bigger picture, instead of getting laser-focused on the details straight away. This perspective is often not considered in a test-after approach.

More specifically, with TDD we

• focus on requirements before writing code.
• must resolve the interface before the implementation.
• develop more modularized code because we must think of the software in terms of small units written and tested independently and integrated together later.

If test-driven development can lead to simpler code, then, ironically, less tests should be needed because of this (under the assumption that simpler code requires less testing).

Type-Driven Development

Ok, now to type-driven development. Type-driven development is a software development practice that puts types first, at the center of what constitutes the act of writing a computer program. In type-driven development, we start by defining the types and type relationships that represent our domain. The type-checker is our assistant in developing our program, giving us immediate feedback. No runtime implementation is written until some sufficient amount of type definitions have been made. As with test-driven development, the process is an iterative spiral, with implementations and type refinement following each other.

On “test-driven development” vs “type-driven development”, Edwin Brady² writes:

There’s a similarity, in that writing tests first helps establish a program’s purpose and whether it satisfies some basic requirements. The difference is that, unlike tests, which can usually only be used to show the presence of errors, types (used appropriately) can show the absence of errors. But although types reduce the need for tests, they rarely eliminate it entirely.

I’m not going to do type-driven development here as much as contrast a more traditional approach to building a solution to what a more type-driven approach would look like. Let’s work with a realistic but very simple problem: we’re writing some web application where users have to sign in with their email.³ Two things the application must do is

1. Verify the user’s email and
2. Provide the ability to reset sign in password

For this we’ll have two business rules:

1. Verification emails must only be sent to customers who have unverified email addresses
2. Password reset emails must only be sent to customers who have verified email addresses

So minimally, we need to capture the email address and information related to verification. Suppose for now that for verification we need to capture two pieces of information:

1. When the email was verified
2. From what IP address is was verified

Let’s start this with a rather naive implementation in a not-uncommon enterprise-OOP style, where we focus on the “data” and “behavior”:

public class Email
{
    readonly string Address;
    readonly string VerificationIp;
    readonly DateTime? VerificationTime;

    public Email(String address, String verificationIp, DateTime? verificationTime)
    {
        Address = address;
        VerificationIp = verificationIp;
        VerificationTime = verificationTime;

    }
    public Boolean IsVerified()
    {
        return (VerificationTime != null) && (VerificationIp != null);
    }

    public void SendVerificationEmail()
    {
        if (IsVerified())
            throw new Exception("Email must be unverified to be verified.");
        // Send the email
        Console.WriteLine("Sending verification email: " + Address);
    }

    public void SendPasswordReset()
    {
        if (!IsVerified())
            throw new Exception("Email must be verified before sending password reset.");
        // Send the email
        Console.WriteLine("Sending passowrd reset: " + Address);
    }
}

This Email class has three attributes:

1. The actual email address
2. VerificationTime to store the date/time on which the verification took place
3. VerificationIp to store the IP address from which the verification took place

The class has an IsVerified method that tells us whether the Email has been verified or not (smell 1). IsVerified checks whether the VerificationTime and VerificationIp have been set (smell 2); if so, the email is verified.

The class also has two more methods:

1. SendVerificationEmail to send out an email if it has not been verified.
2. SendPasswordReset to send an email to reset a password if it has been verified.

If the conditions are not met, both functions throw an exception (smell 3).

Let’s look at the problems in this code.

• smell 2: The way we know that the email is verified is by checking that both VerificationTime and VerificationIp are set. If neither is set, the email is not verified. But also if only one of the two is set, the email won’t be verified. Why would we have one set and not the other? Is that a valid state for the Email to be in? If not, the code should better not allow this.
• smell 3: Functions SendVerificationEmail and SendPasswordReset operate on the internal values of an Email object, so in order to enforce the business rules, they need to check the verification status of the email to do or do not do. Regrettably they throw exceptions when the state is invalid for the given operation, making the functions partial and the type signature inconsistent with the behavior of the function, and thus forcing the user to know about some implementation details.
• smell 1: Having a method to check verification status seems not only harmless, but reasonable. However, it has a couple of problems. First, if tomorrow we decide to add another attribute related to verification, we’ll have to remember to update this IsVerified method for it to continue being correct. Second, it introduces unnecessary runtime branching logic that adds complexity; this can be replaced by compile time checks. We’ll see how to do this in a minute.

Let’s now improve our implementation with a type-driven approach. But before we do that, let’s translate our code to a more capable (and palatable) language (this C# code is a bit nauseating :-). Here’s essentially the same thing in F#:

module Email_0 =

    type Email = 
        { Address: string; VerificationIp: string option; VerificationTime: DateTime option }

        member this.IsVerified = 
            this.VerificationTime.IsSome && this.VerificationIp.IsSome

        member this.SendVerificationEmail () =
            if this.IsVerified then
                raise (Exception "Email must be unverified to be verified.")
            else
                // Send email
                printfn "send verification email"

        member this.SendPasswordReset () =
            if not this.IsVerified then
                raise (Exception "Email must be verified before sending password reset.")
            else
                // Send email
                printfn "send passowrd reset"

Note that in IsVerified I misuse the option type on purpose to keep parity with the C# implementation; we’ll fix this. Let’s address each of the “smells” in turn:

smell 2: make invalid states unrepresentable (and un-runnable)

The fact that the two email verification attributes can be set independently (causing our email objects to be in an invalid state where only part of the verification information exists) is a problem. For example, there’s nothing stopping us from setting the VerificationIp without setting the VerificationTime. We can fix this easily by changing the definition of the Email type to be a sum of two values: an UnverifiedEmail, which only holds the email address, and a VerifiedEmail, which holds the address and the verification information:

    type Email =
        | UnverifiedEmail of string
        | VerifiedEmail of
            {| Address: string
               Timestamp: DateTime
               Ip: string |}

Now it is impossible to create an Email value with an invalid state or nonsensical value combinations; a VerifiedEmail must always have a verification time and an IP.

smell 3: make functions total

Let’s improve the email sending functions based on this change. Let’s start by extracting them from the Email type. i.e., instead of being member methods, they will be pure functions that have an Email as parameter (The reason of this will become apparent in a minute).

    let sendVerificationEmail email =
        match email with
        | UnverifiedEmail email -> printfn "send verification email: %A" email
        | VerifiedEmail _ ->
            // do nothing
            ()

    let sendPasswordReset email =
        match email with
        | UnverifiedEmail _ ->
            // ignore
            ()
        | VerifiedEmail email -> printfn "send password reset: %A" email

Note that the IsVerified function is no longer relevant given our new definition of Email, so we can ditch it. To see if Email is verified or not, we just match on the two values of it’s definition and act according to the value. Another improvement made is that we’re no longer throwing exceptions, but are always returning instead. This makes our functions total and our function signatures correct (i.e., we can trust that the signature Email -> () always holds. i.e., the functions will always take an Email and return a unit; no exceptions, no surprises. )

smell 1: no run time branching + make invalid states unrepresentable

Let’s now reify the two email verification status values as types and use them to enforce, at compile time, the domain rules around sending verification and password reset emails. While we’re at it, let’s also replace the generic string type associated with the email address and the verification IP with more specific domain types. This now prevents us from accidentally assigning an IP to an email address and vice versa:

module Email_2 =
    type EmailAddress = EmailAddress of string
    type Ip = Ip of string

    type UnverifiedEmail = EmailAddress
    type VerifiedEmail =
        { Address: EmailAddress
          Timestamp: DateTime 
          Ip: Ip}

    type Email =
        | Unverified of UnverifiedEmail
        | Verified of VerifiedEmail

    let sendVerificationEmail (email: UnverifiedEmail) =
        printfn "send verification email: %A" email

    let sendPasswordReset (email: VerifiedEmail) = printfn "send password reset: %A" email

We’ve changed the email sending functions so that they have as parameter the type that corresponds to the email status required. Now no runtime check is needed or performed.

These small changes have taken our code from one that allows invalid states, has partial functions that throw exceptions and have false signatures, and has superfluous runtime branching, to one where the domain logic is clear in the types and enforced by the type checker, and where it’s impossible to execute invalid actions according to the domain rules. This is what type-driven development is about. Types as first-class language constructs; types at the center of the domain encoding; types as the reification of (part of) the domain.

Let’s summarize some of the benefits of type-driven development:

1. Type-driven development reduces runtime test requirements. Just like TDD reduces debugging, type-driven development reduces testing.
2. Faster feedback loop: The feedback loop provided by the compiler is even faster than that provided by runtime tests.
3. Better design: Focusing on the types first means focusing on the interfaces and their interdependencies. Code can be modularized before writing a single line of runtime code.
   
4. Better collaboration and communication: Types act as a common language between stakeholders, developers, and the compiler.

This has been a very brief and shallow intro to driving software development with types. Types are powerful and I hope I could convey this with my example.