Implication as Function Types

The most fundamental correspondence is between logical implication and function types. Consider the proposition "If it rains, then the ground is wet" (P ⇒ Q). In type theory, this becomes a function type Rain → Wet.

// The proposition "P implies Q" as a function type
type Implication<P, Q> = (p: P) => Q;

// A proof that "if we have an A, we can get a B"
function proofOfImplication<A, B>(): (a: A) => B {
  // This is a proof template - the implementation
  // constructs the proof
  return (a: A): B => {
    // Proof construction here
    throw new Error("Proof needed");
  };
}

// Example: Proof of transitivity (A → B) → (B → C) → (A → C)
function transitivity<A, B, C>(
  f: (a: A) => B,
  g: (b: B) => C
): (a: A) => C {
  return (a: A) => g(f(a));
}

Conjunction as Product Types

The logical conjunction "P and Q" (P ∧ Q) corresponds to the product type (pair). To prove P ∧ Q, you need both a proof of P and a proof of Q.

// Conjunction as a pair type
type And<P, Q> = [P, Q];

// Proof that P ∧ Q implies P (first projection)
function andElimLeft<P, Q>(proof: And<P, Q>): P {
  return proof[0];
}

// Proof that P ∧ Q implies Q (second projection)
function andElimRight<P, Q>(proof: And<P, Q>): Q {
  return proof[1];
}

// Proof that P → Q → (P ∧ Q) (pair introduction)
function andIntro<P, Q>(p: P, q: Q): And<P, Q> {
  return [p, q];
}

// Proof that (P ∧ Q) → (Q ∧ P) (commutativity)
function andCommutative<P, Q>(proof: And<P, Q>): And<Q, P> {
  return [proof[1], proof[0]];
}

Disjunction as Sum Types

The logical disjunction "P or Q" (P ∨ Q) corresponds to sum types (tagged unions). To prove P ∨ Q, you need either a proof of P or a proof of Q.

// Disjunction as a tagged union
type Or<P, Q> = 
  | { tag: "left"; value: P }
  | { tag: "right"; value: Q };

// Proof that P implies (P ∨ Q)
function orIntroLeft<P, Q>(p: P): Or<P, Q> {
  return { tag: "left", value: p };
}

// Proof that Q implies (P ∨ Q)
function orIntroRight<P, Q>(q: Q): Or<P, Q> {
  return { tag: "right", value: q };
}

// Proof by cases: (P ∨ Q) → (P → R) → (Q → R) → R
function orElim<P, Q, R>(
  proof: Or<P, Q>,
  onLeft: (p: P) => R,
  onRight: (q: Q) => R
): R {
  if (proof.tag === "left") {
    return onLeft(proof.value);
  } else {
    return onRight(proof.value);
  }
}

Natural Deduction Rules as Typing Rules

// AXIOM RULE (Variable)
// In natural deduction: If P is assumed, then P is proven
// In type theory: If x has type A in context, then x has type A
function identity<A>(x: A): A {
  return x;  // The simplest proof: assumption proves itself
}

// IMPLICATION INTRODUCTION (→I, Abstraction)
// To prove P → Q, assume P and prove Q
// To construct a function A → B, take parameter of type A and return B
function implIntro<A, B>(proof: (a: A) => B): (a: A) => B {
  return proof;  // λ-abstraction
}

// IMPLICATION ELIMINATION (→E, Application, Modus Ponens)
// If we have P → Q and P, we can derive Q
// If we have f: A → B and a: A, we can get f(a): B
function implElim<A, B>(f: (a: A) => B, a: A): B {
  return f(a);  // Function application
}

Example: Proving the K Combinator

The K combinator (constant function) proves the theorem P → (Q → P):

// K combinator: λx.λy.x
// Type: A → B → A
// Logical reading: P → (Q → P)
// Meaning: "If P is true, then P is true regardless of Q"
function K<A, B>(x: A): (y: B) => A {
  return (y: B) => x;
}

// This is a proof that if we have a proof of P,
// we can always produce a proof of P even when given
// an additional hypothesis Q

Example: Proving the S Combinator

The S combinator proves a more complex theorem:

// S combinator: λx.λy.λz.x z (y z)
// Type: (A → B → C) → (A → B) → A → C
// Logical reading: (P → Q → R) → (P → Q) → P → R
function S<A, B, C>(
  x: (a: A) => (b: B) => C
): (y: (a: A) => B) => (z: A) => C {
  return (y: (a: A) => B) => (z: A) => x(z)(y(z));
}

// This proves: "If P implies (Q implies R), and P implies Q,
// then P implies R"
// This is a form of hypothetical syllogism

Dependent Function Types (Π-types)

A dependent function type Πx:A.B(x) represents a function that, given x of type A, returns a value of type B(x) where B depends on x. This corresponds to universal quantification ∀x:A.P(x).

// Pseudo-TypeScript with dependent types (like in Agda/Coq/Lean)
// This isn't valid TypeScript, but illustrates the concept

// Universal quantification: ∀n:Nat. P(n)
// As a dependent function: (n: Nat) => P(n)
interface Vec<T, N extends number> {
  // Vector of length N
}

// Proof that ∀n. Vec<T, n> can be reversed to Vec<T, n>
function reverse<T, N extends number>(vec: Vec<T, N>): Vec<T, N> {
  // Implementation preserves length in the type
  return vec; // simplified
}

Dependent Pair Types (Σ-types)

A dependent pair type Σx:A.B(x) represents a pair (x, y) where x has type A and y has type B(x). This corresponds to existential quantification ∃x:A.P(x).

// Existential quantification: ∃n:Nat. Vec<T, n>
// "There exists a natural number n such that we have a vector of length n"
interface ExistsVec<T> {
  length: number;  // The witness: a specific n
  vector: Vec<T, typeof this.length>;  // Proof that Vec<T, n> holds for this n
}

// Constructing an existential proof
function singleton<T>(value: T): ExistsVec<T> {
  return {
    length: 1,  // We choose n = 1 as our witness
    vector: [value] as any  // And provide a vector of that length
  };
}

Example in Agda-like Syntax

-- Agda-like pseudocode
-- Proving that vector append has the right length

data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)

-- The type of append PROVES that lengths add up
_++_ : {A : Set} {m n : Nat} → Vec A m → Vec A n → Vec A (m + n)
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

-- The type signature is a theorem:
-- "For all types A and numbers m, n,
--  if you have a vector of length m and a vector of length n,
--  then you can produce a vector of length m+n"
-- The function definition is the PROOF of this theorem!

Example: Proving List Properties in Coq

(* Coq proof that list reversal is involutive *)
Require Import List.
Import ListNotations.

(* Helper lemma: reverse of append *)
Lemma rev_append_distr : forall A (l1 l2 : list A),
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros A l1 l2.
  induction l1 as [| h1 t1 IH].
  - (* l1 = [] *)
    simpl.
    rewrite app_nil_r.
    reflexivity.
  - (* l1 = h1 :: t1 *)
    simpl.
    rewrite IH.
    rewrite app_assoc.
    reflexivity.
Qed.

(* Main theorem: reverse is involutive *)
Theorem rev_involutive : forall A (l : list A),
  rev (rev l) = l.
Proof.
  intros A l.
  induction l as [| h t IH].
  - (* l = [] *)
    simpl.
    reflexivity.
  - (* l = h :: t *)
    simpl.
    rewrite rev_append_distr.
    rewrite IH.
    simpl.
    reflexivity.
Qed.

Each Proof block is a program that constructs evidence for the theorem. The tactics (intros, induction, rewrite, reflexivity) are instructions for building this proof term.

Example: Arithmetic in Lean 4

-- Lean 4 proof that addition is commutative
theorem add_comm (m n : Nat) : m + n = n + m := by
  induction n with
  | zero =>
    -- Base case: m + 0 = 0 + m
    rw [Nat.add_zero, Nat.zero_add]
  | succ n ih =>
    -- Inductive case: m + (n+1) = (n+1) + m
    rw [Nat.add_succ, ih, Nat.succ_add]

-- Proof that multiplication distributes over addition
theorem mul_add (m n k : Nat) : m * (n + k) = m * n + m * k := by
  induction k with
  | zero =>
    rw [Nat.add_zero, Nat.mul_zero, Nat.add_zero]
  | succ k ih =>
    rw [Nat.add_succ, Nat.mul_succ, ih, Nat.mul_succ, Nat.add_assoc]

-- Using dependent types to prove vector properties
def Vec (α : Type) (n : Nat) := { l : List α // l.length = n }

def vappend {α : Type} {m n : Nat} (v1 : Vec α m) (v2 : Vec α n) : Vec α (m + n) :=
  ⟨v1.val ++ v2.val, by
    simp [List.length_append, v1.property, v2.property]⟩

Session Types

Linear types enable session types, which ensure protocol correctness at compile time:

// Simplified session types in Rust
// State machine encoded in types

struct Initialized;
struct Authenticated;
struct Closed;

struct Connection<State> {
    _phantom: std::marker::PhantomData<State>,
    socket: std::net::TcpStream,
}

impl Connection<Initialized> {
    fn new(addr: &str) -> std::io::Result<Self> {
        Ok(Connection {
            _phantom: std::marker::PhantomData,
            socket: std::net::TcpStream::connect(addr)?,
        })
    }
    
    // State transition: Initialized → Authenticated
    fn authenticate(self, credentials: &str) -> Connection<Authenticated> {
        // Perform authentication...
        Connection {
            _phantom: std::marker::PhantomData,
            socket: self.socket,
        }
    }
}

impl Connection<Authenticated> {
    // Only authenticated connections can send messages
    fn send_message(&mut self, msg: &str) -> std::io::Result<()> {
        // Send message...
        Ok(())
    }
    
    // State transition: Authenticated → Closed
    fn close(self) -> Connection<Closed> {
        Connection {
            _phantom: std::marker::PhantomData,
            socket: self.socket,
        }
    }
}

// Usage enforces correct protocol:
fn use_connection() -> std::io::Result<()> {
    let conn = Connection::new("localhost:8080")?;
    // conn.send_message("hi")?;  // ERROR: not authenticated!
    
    let mut conn = conn.authenticate("secret");
    conn.send_message("Hello")?;  // OK: authenticated
    
    let conn = conn.close();
    // conn.send_message("bye")?;  // ERROR: connection closed!
    Ok(())
}

1. Verified Compilers

CompCert is a formally verified C compiler written in Coq. Its correctness is a proven theorem:

Theorem transf_c_program_correct:
  forall p tp,
  transf_c_program p = OK tp ->
  forward_simulation (Csem.semantics p) (Asm.semantics tp).

This theorem states: "If the compiler successfully compiles program p to tp, then the assembly semantics of tp is a forward simulation of the C semantics of p." The proof of this theorem IS the compiler.

2. Verified Operating Systems

seL4 is a formally verified microkernel. Properties like "isolation between processes" are proven theorems:

theorem integrity:
  "⟦ valid_state s; (s, s') ∈ data_type.step; pas_wellformed pas ⟧
   ⟹ (∀d∈subjects_of_state s. integrity_check s s' d pas)"

3. Smart Contract Verification

Using Curry-Howard to verify smart contracts:

// Property we want to prove:
// "After a valid transfer, sender balance decreases and receiver balance increases"
interface Transfer {
  from: Address;
  to: Address;
  amount: bigint;
}

interface BalanceState {
  balances: Map<Address, bigint>;
}

// The theorem (as a type)
type TransferPreservesInvariant = (
  state: BalanceState,
  transfer: Transfer
) => [
  BalanceState,  // New state
  Proof<
    And<
      Equals<Balance(newState, transfer.from), Balance(state, transfer.from) - transfer.amount>,
      Equals<Balance(newState, transfer.to), Balance(state, transfer.to) + transfer.amount>
    >
  >
];

// The function implementation IS the proof
function executeTransfer(
  state: BalanceState,
  transfer: Transfer  
): [BalanceState, /* proof */] {
  const newBalances = new Map(state.balances);
  
  const fromBalance = newBalances.get(transfer.from) || 0n;
  const toBalance = newBalances.get(transfer.to) || 0n;
  
  // The fact that this compiles proves the invariant holds
  newBalances.set(transfer.from, fromBalance - transfer.amount);
  newBalances.set(transfer.to, toBalance + transfer.amount);
  
  return [{ balances: newBalances }, /* proof witness */];
}

4. Type-Safe Database Queries

Libraries like Prisma use the Curry-Howard correspondence to ensure query safety:

// The type system proves that this query is well-formed
const result = await prisma.user.findMany({
  where: {
    age: { gt: 18 },  // Type-checked: age is number
    email: { contains: "@" },  // Type-checked: email is string
  },
  select: {
    id: true,
    name: true,
    // posts: true,  // If uncommented, return type automatically includes posts
  },
});

// Result type is automatically inferred as:
// Array<{ id: number; name: string }>
// The type system has PROVEN that only id and name are selected

1. Correctness is Compositional

Just as you can build complex proofs from simpler lemmas, you can build correct programs from correct components. Type safety guarantees this composition preserves correctness.

// If f: A → B is correct (proves P → Q)
// And g: B → C is correct (proves Q → R)
// Then g ∘ f: A → C is automatically correct (proves P → R)
function compose<A, B, C>(
  f: (a: A) => B,
  g: (b: B) => C
): (a: A) => C {
  return (a: A) => g(f(a));
  // Correctness is FREE - it follows from types
}

2. The Uncomputable is Unprovable

By Gödel's incompleteness theorems, there exist true statements that cannot be proven. By Curry-Howard, there exist types that have no inhabitants (no programs of that type).

// The halting problem: no function can decide if arbitrary programs halt
// This corresponds to the logical statement being unprovable
type Program = string;
type Input = string;

// This type has NO inhabitants (cannot be implemented):
type HaltingOracle = (p: Program, input: Input) => boolean;
// We cannot write a total function with this type

3. Types as Contracts

A type signature is a contract—a precise specification of what a function promises. The implementation is a proof that the contract can be fulfilled.

-- Haskell: the type signature is a theorem
-- The implementation is the proof

-- Theorem: "Lists form a monoid under concatenation"
instance Monoid [a] where
  mempty = []  -- Proof of identity element
  mappend = (++)  -- Proof of associative operation

-- The type checker verifies this proof is correct