The Curry-Howard Correspondence: when types become proofs

In the Making Invalid States Unrepresentable 1. Why boolean flags are bugs in disguise series, we saw that sum types (enums) encode domain states precisely, while boolean flags create exponential explosions of nonsense values. But there is a deeper reason why this works, and it comes from a theorem discovered decades before Rust, TypeScript, or even Java existed.

Types are propositions. Programs are proofs.

#

The Curry-Howard correspondence, discovered by Haskell Curry (1934) and William Alvin Howard (1969), establishes a direct mapping between logic and type theory:

This is not a loose analogy. It is an isomorphism: every statement on the left has a precise counterpart on the right, and vice versa.

What this means in practice

#

When you write a type definition, you are stating a proposition. When you construct a value of that type, you are providing a proof.

Consider this enum:

enum Light {
    Red,
    Green,
    Yellow,
}

The proposition: “A traffic light is in exactly one of three states: Red, Green, or Yellow.”

Every time you create a Light::Red, you are constructing a proof that the proposition holds. The compiler verifies this proof at every use site via exhaustive pattern matching: if you match on a Light and forget Yellow, the proof is incomplete, and the compiler rejects it.

Now compare with booleans:

struct Light {
    is_red: bool,
    is_green: bool,
    is_yellow: bool,
}

The proposition: “A traffic light has some combination of red, green, and yellow flags.” This is a much weaker claim. It says nothing about exclusivity. The “proof” (any value of this type) includes Light { is_red: true, is_green: true, is_yellow: false }, which proves a proposition that is true in the type system but false in reality.

The function type as implication

#

A function A -> B corresponds to the logical implication “if A then B.” A function that transforms one type into another is a proof that the first proposition implies the second.

fn ship_order(order: PaidOrder) -> ShippedOrder {
    // ...
}

This function is a proof of the proposition: “If an order is paid, then it can be shipped.” The type system guarantees that you cannot call this function with a CancelledOrder. The implication holds by construction.

If the function took a struct with boolean flags instead, the proposition would be: “Given some combination of boolean flags, you get some other combination.” That proves almost nothing about your domain.

Why ! (Never) matters

#

The empty type ! in Rust (or Void in Haskell) has zero values. Under Curry-Howard, it corresponds to False, a proposition with no proof. You cannot construct a value of type ! because there is no proof of False.

This is why match expressions with ! require no branches: if a value cannot exist, there is nothing to handle. The Rust compiler understands this:

fn absurd(x: !) -> String {
    match x {
        // No branches needed -- x cannot exist
    }
}

A function from ! to anything is always valid (vacuously true: “if False then anything” is a theorem in logic). This is known as the ex falso quodlibet principle.

Correct by construction

#

In formal methods, correct by construction means building a system such that invalid behaviors are structurally impossible, rather than building it and then verifying post-hoc.

Making invalid states unrepresentable is the type-level manifestation of this principle. Instead of writing the code and then testing that impossible states never occur, you design the types so that impossible states cannot be expressed in the first place.

There is a hierarchy of how much guarantee you get:

Most production software operates at levels 3 and 4. Moving from level 4 to level 3, from runtime checks to compile-time type partitioning, is the single highest-leverage improvement you can make in type safety. It is free at runtime, requires no external tools, and works in every language with sum types.

Refinement types: the next step up

#

Refinement types carry predicates: {x: Int | x > 0} describes a positive integer. Languages like Liquid Haskell and F* support these directly. The compiler not only checks that you have an Int, but also verifies that the predicate holds.

Sum types approximate refinement types at a coarser granularity. Instead of arbitrary predicates, they partition the domain into named, finite cases. An enum with five variants is not as precise as a refinement type with an arbitrary predicate, but it is infinitely more precise than a product of booleans.

The practical insight: you do not need dependent types or formal theorem provers to get most of the benefit. The jump from “bag of booleans” to “well-chosen enum” eliminates entire classes of bugs, and every mainstream language supports it today.

The takeaway

#

The Curry-Howard correspondence tells us that the relationship between types and correctness is not a vague metaphor. Types are propositions. Programs are proofs. When you choose a sum type over a product of booleans, you are making a stronger logical claim about your domain, and the compiler proves that claim on every build.

Correct by construction is not just a slogan. It is a design practice: choose types that make the impossible inexpressible, and let the compiler do the verification for free.