For many programmers, precise mathematical logic and general programming feel like different worlds.

• Logic is about proving theorems.
• Programming is about making systems behave correctly.
• Proofs belong to mathematicians.
• Functions belong to engineers.

But in systems like Lean, those boundaries start collapsing.

One of the deepest ideas behind this is the Curry–Howard correspondence -- the observation that:

• logical propositions correspond to types
• proofs correspond to programs
• proof checking corresponds to type checking

At first, this sounds abstract, philosophical, or even like category theory mysticism.

But once you see it expressed concretely in Lean, it becomes quite mechanical.

This article walks through that transition step by step:

• from logic,
• to functions,
• to proof goals,
• to types carrying specifications,
• to a sorting function that literally contains its own correctness proof.

The Core Idea: Propositions Behave Like Types

Let us start with a tiny logical statement:

P ∧ Q → P

Read logically, this means:

“If P and Q are both true, then P is true.”

Very obvious.

Now let us reinterpret it computationally.

Logical Interpretation

To prove:

P ∧ Q

you must provide:

• a proof of P
• and a proof of Q

That structure is identical to a pair:

(p, q)

Similarly, to prove:

P → Q

you must provide:

• a method that transforms evidence of P
• into evidence of Q

That is exactly what a function does.

So under Curry–Howard:

This is not metaphorical in Lean.

It is literal.

A Tiny Theorem Is Also a Program

Here is a theorem in Lean:

theorem fst : P ∧ Q → P := by
  intro h
  exact h.left

Let us read this slowly.

The Goal

Initially Lean shows:

⊢ P ∧ Q → P

Everything after ⊢ is the current proof goal.

You can think of it as:

“Construct something of this type.”

Step 1: intro h

intro h

This assumes:

h : P ∧ Q

and changes the goal to:

⊢ P

So now we have evidence that:

• P is true
• Q is true

bundled inside h.

Step 2: Extract the Left Side

exact h.left

This extracts the proof of P.

Done.

Now look at the exact same theorem computationally.

The theorem is equivalent to:

fun h => h.left

This is just:

• take a pair
• return the first element

The same object is simultaneously:

• a proof,
• and a program.

That is Curry–Howard.

Lean Proof Goals Are Requests for Evidence

A useful way to think about Lean is:

Lean is constantly asking you for evidence.

Suppose Lean shows:

⊢ Sorted ys

This is not a boolean check.

Lean is not asking:

“Is this true?”

It is asking:

“Can you construct evidence that this is true?”

That distinction matters enormously.

In ordinary programming:

• correctness is often informal,
• hidden in comments,
• or validated through testing.

In Lean:

• correctness becomes part of the type system itself.

Types Can Express Specifications, Not Just Data Shapes

Most programmers are used to types like:

sort : List Nat -> List Nat

This only says:

• input: list
• output: list

Nothing about correctness.

The function could:

• reverse the list,
• shuffle the list,
• return garbage,
• or always return [].

The type would still accept it.

Now look at this:

sort :
  (xs : List Nat) ->
  { ys : List Nat //
      Sorted ys ∧ Permutation xs ys }

This changes everything.

The function is now required to produce:

1. an output list ys
2. a proof that ys is sorted
3. a proof that ys contains exactly the same elements as xs

The type stopped describing shape and started describing truth.

“Sorted” Becomes a Logical Object

But where does Sorted come from?

It must itself be formally defined.

Here is a simplified version:

inductive Sorted : List Nat -> Prop
| nil :
    Sorted []

| single (x : Nat) :
    Sorted [x]

| cons (x y : Nat) (xs : List Nat) :
    x ≤ y ->
    Sorted (y :: xs) ->
    Sorted (x :: y :: xs)

This says:

• empty lists are sorted
• single-element lists are sorted

• larger lists are sorted if:

  • the first element is ≤ the second
  • and the tail is sorted

Now suppose your implementation returns:

[1,2,3]

Lean must construct evidence for:

Sorted [1,2,3]

That proof is itself a structured object.

Roughly:

1 ≤ 2
2 ≤ 3
tail sorted

all recursively assembled together.

What Happens When the Function Is Wrong?

Suppose the implementation returns:

[3,1,2]

Lean now tries to construct:

Sorted [3,1,2]

But according to the definition of Sorted, this eventually requires:

proof(3 ≤ 1)

Impossible.

So the program is rejected.

Notice what happened here.

We did not:

• run tests,
• inspect runtime output,
• fuzz inputs,
• or hope for good behavior.

Instead:

• the implementation failed to inhabit the required type.

The proof could not be constructed.

So the program was invalid.

The Deep Shift: Correctness Became Construction

This is the conceptual leap Curry–Howard enabled.

Traditionally:

• programs were operational artifacts,
• proofs were human reasoning artifacts.

Curry–Howard showed they share the same structure.

That insight led to:

• proof assistants,
• dependently typed programming,
• formally verified kernels,
• verified compilers,
• machine-checked mathematics,
• cryptographic verification systems.

The key shift is this:

A proof is not merely an argument.

It is a concrete computational object.

And in Lean:

• writing a program
• and proving it correct

can become the same act.

Closing Thoughts

When people first hear:

“propositions are types”

“proofs are programs”

it often sounds like abstract mathematical poetry.

But Lean makes the idea concrete.

A theorem becomes a type.
A proof becomes a value.
A function becomes logical implication.
And type checking becomes proof verification.

The result is a system where correctness is not merely documented or tested after the fact.

It becomes part of what the program is.

That is the real significance of the Curry–Howard correspondence:

• not philosophy for its own sake,
• but a bridge between logic and executable systems.

And once you see it inside Lean, it becomes difficult to unsee.