ProofScript Programming Language

Type Theory in ProofScript

Why the theory behind Lean and ProofScript is worth learning.

Home · Docs · Type Theory · Proofs · Verified Software · ProofScript → Lean + TypeScript · Reference · Examples · Download

Dependent type theory can sound like a subject you need a mathematics degree to approach. You do not. The central ideas can be built from programming concepts you already know: values, types, functions, data constructors, pattern matching, and function composition.

The surprising part is how far those ideas can go.

Syntax note: examples aimed at TypeScript developers may use function and top-level const; both are aliases for canonical def definitions. The type theory underneath is unchanged.

Before the theory: one rule for reading this page

You are not expected to know symbols such as →, ∀, ∃, Prop, Type, or words such as inhabitant, recursor, and impredicative before reading this page.

Each concept follows this order:

ordinary programming intuition
→ code
→ English reading
→ why the idea matters
→ formal name

For example, when you see:

(n: Nat) → Fin(n + 1)

first read it as:

“Give me a natural number n; I return a natural number that is guaranteed to be below n + 1.”

Only after that do you need the formal phrase dependent function type.

Lean’s own theorem-proving text introduces dependent type theory as a language for mathematical assertions, software/hardware specifications, and proofs. ProofScript v0.1 deliberately targets Lean 4.33.1 semantics while reshaping parts of the source syntax for TypeScript-oriented readability. See Theorem Proving in Lean 4 — Dependent Type Theory and the Lean Language Reference — The Type System.

1. Start with the ordinary idea: values have types

42 : Nat

Read:

“42 has type Nat.”

This is the basic typing judgment you already use informally in TypeScript.

const count: number = 42;

In ProofScript:

const count: Nat := {
  42
}

The surface looks familiar, but Nat has a mathematical source-level meaning: natural numbers.

Why care about that distinction? Because formal reasoning depends on knowing what operations mean. If “number” sometimes means floating-point arithmetic, sometimes arbitrary integers, and sometimes runtime coercion, a theorem about arithmetic needs a precise model. ProofScript keeps foundational numeric types explicit.

2. Types are themselves terms

Now take one conceptual step upward:

42  : Nat
Nat : Type

The first line says 42 is classified by Nat.

The second says Nat itself is classified by Type.

This is one of the gateways into dependent type theory. A type is not merely external compiler metadata. Types live inside the theory strongly enough that functions can abstract over them.

function identity{A: Type}(x: A): A := {
  x
}

In English: “For any type A, take a value x of type A and return a value of the same type.”

Compare TypeScript:

function identity<T>(x: T): T {
  return x;
}

The generic idea is familiar. What changes is how deeply types can interact with ordinary values and propositions.

3. Function types are the backbone

Ordinary function type:

A → B

Read:

“A function from A to B.”

If:

f : A → B
x : A

then applying f to x gives:

f(x) : B

This same function-space idea will later express logical implication.

4. The key move: let the output type depend on the input value

Ordinary function:

Nat → Nat

The result type is always Nat.

Dependent function:

(n: Nat) → Fin(n + 1)

Read slowly:

  1. (n: Nat) — the input is named n and has type Nat.
  2. → — “produces.”
  3. Fin(n + 1) — the output type contains the particular input value n.

So the whole type means:

“For each natural number n, return a bounded natural that is strictly less than n + 1.”

Because the output type changes with n, this is a dependent function type. In formal terminology it is a Pi type.

Do not let the terminology hide the simple idea: the result type is allowed to mention the input.

5. Fin(n): the smallest useful dependent-type example

Fin(n) is a natural number with evidence that its value is less than n.

Conceptually:

Fin(5)

contains only:

0, 1, 2, 3, 4

but the important part is not “a runtime integer with a range check.” The important part is that the bound participates in the type.

Example:

def lastIndex{n: Nat}(h: 0 < n): Fin(n) := {
  ⟨n - 1, by omega⟩
}

In English

“For any positive natural number n, return n - 1 together with a proof that n - 1 < n.”

Why this matters

Suppose an indexing API expects:

Fin(xs.size)

Then a valid index is not merely “some number that we hope is in range.” Its type is connected to the size of this particular xs.

That relationship is what dependent typing buys you.

6. From Fin to length-indexed data

Consider a vector type:

Vector(A, n)

Read:

“A vector of elements of type A whose length is n.”

Now an append function can express a stronger result type:

Vector(A, n)
→ Vector(A, m)
→ Vector(A, n + m)

Read:

“Append a vector of length n to a vector of length m; the result has length n + m.”

The arithmetic relationship appears in the type itself.

In an ordinary type system you might write:

function append<A>(left: A[], right: A[]): A[]

which correctly describes element types but not the length equation.

Dependent types can move selected invariants from documentation into checked interfaces.

7. Refinement intuition: types as increasingly precise descriptions

A helpful ladder is:

number-like value
      ↓
Nat
      ↓
Fin(10)
      ↓
Fin(xs.size)

Each step narrows the allowed values or ties them to more context.

Then take one more step:

Sorted(xs)

Now we are no longer merely classifying a value—we are stating a proposition about it.

And then:

proof : Sorted(xs)

means we possess checked evidence for the property.

This is why type theory is not academic decoration in ProofScript. It provides a continuum from basic typing to formal specification.

8. Propositions are types

Lean-style dependent type theory uses a special universe of propositions:

Prop

A proposition such as:

2 + 2 = 4

has type:

Prop

We can write:

2 + 2 = 4 : Prop

Now suppose:

h : 2 + 2 = 4

Because the type of h is the proposition, h is a proof of that proposition.

This viewpoint is usually called propositions as types.

The larger correspondence between logic and typed programs is commonly associated with Curry–Howard. You do not need the name to use the idea.

The useful intuition is:

proposition = type of acceptable evidence
proof       = value inhabiting that type

9. “Inhabits” just means “is a valid value of the type”

Formal texts often say:

“h inhabits P.”

For a beginner, read that as:

“h is a valid value of type P.”

If P : Prop, then being a value of type P means h is a proof of P.

So:

h : P

can be read:

“h is evidence that P holds.”

10. Implication becomes a function

Suppose:

P : Prop
Q : Prop

What would it mean to prove:

P → Q

Under propositions-as-types, it means constructing a function:

proof of P
    ↓
proof of Q

That is exactly what implication says: if P holds, then Q holds.

ProofScript example:

theorem identityImplication(P: Prop): P → P := by {
  intro h
  exact h
}

In English

“For any proposition P, if you give me a proof of P, I can produce a proof of P: I return the same evidence.”

The proof is function construction.

11. Universal quantification becomes dependent function space

Mathematics writes:

∀ x: A, P(x)

Read:

“For every x of type A, P(x) holds.”

In dependent function notation:

(x: A) → P(x)

Read computationally:

“Given any x: A, construct a proof of P(x).”

That is the same underlying Pi-type mechanism used earlier for:

(n: Nat) → Fin(n + 1)

One framework serves both programming and logic.

12. Existential quantification is witness + evidence

Mathematics writes:

∃ x: A, P(x)

Read:

“There exists an x of type A such that P(x) holds.”

A constructive proof generally supplies:

some x : A
+
proof : P(x)

So existence is not necessarily a vague assertion. It can contain a concrete witness and evidence that the witness works.

This is related to dependent pair/Sigma types, where the type of the second component depends on the first.

13. Bool and Prop: computation versus logical evidence

This is worth repeating because many programming languages blur the intuition.

Boolean

x == y : Bool

This is a computation that produces true or false through Boolean equality.

Proposition

x = y : Prop

This is a mathematical statement that can have a proof.

A Boolean decision procedure can sometimes be connected to a proposition by a theorem, but the two concepts are not identical by default.

A useful pattern is:

Boolean test
    ↕ theorem proving correspondence
Proposition

That theorem is what justifies using the computation as evidence for the proposition.

14. Why := and = must remain different

In a theorem prover, equality is not just assignment syntax.

Definition:

def answer: Nat := {
  42
}

Read:

“Define answer as 42.”

Proposition:

answer = 42

Read:

“answer is mathematically equal to 42.”

Proof:

theorem answerCorrect: answer = 42 := by {
  rfl
}

The theorem uses both:

This visible separation helps preserve the distinction between syntax that introduces something and logic that talks about something.

15. Definitional equality: computation can make expressions the same

There are equalities you can prove because both sides compute to the same core expression.

function double(n: Nat): Nat := {
  n + n
}

Then:

double(2)

unfolds/computes to:

2 + 2

and then to:

4

So:

theorem doubleTwo: double(2) = 4 := by {
  rfl
}

can be proved by reflexivity.

The checker’s built-in notion that expressions reduce to the same thing is called definitional equality.

The proposition double(2) = 4 is propositional equality.

These interact, but they are conceptually distinct.

16. Beta reduction: function application computes

A lambda function:

fun x => x + 1

applied to 4:

(fun x => x + 1)(4)

reduces to:

4 + 1

This substitution step is commonly called beta reduction.

You do not need to memorize the term immediately. The practical idea is:

The core type checker knows how certain expressions compute, and this computation participates in checking types and proofs.

That is one reason proofs can be concise: sometimes the theorem follows directly from computation.

17. Inductive types: describe data by how it can be built

An inductive type introduces constructors.

Schematic example:

inductive TrafficLight {
  | red;
  | yellow;
  | green;
}

Every TrafficLight value comes from one of those constructors.

This gives you two dual powers.

Programming

To compute from a TrafficLight, inspect which constructor built it.

Proof

To prove a property about every TrafficLight, prove the property for each constructor.

That is why inductive types sit at the center of both programming and proving.

Lean connection: why inductive types matter so much

Lean’s official reference describes inductive types as its primary mechanism for introducing new types. From the constructors, Lean derives a recursor. The same recursor has two faces:

computational reading → primitive recursive computation
logical reading       → induction / elimination principle

That is why ProofScript can present recursion and induction as related ideas rather than two unrelated language features.

Official background: Lean Language Reference — Inductive Types.

18. Lists show recursion and induction as two views of the same structure

A list is built from constructors conceptually like:

[]
head :: tail

A recursive function follows this shape:

def length{A: Type}: List(A) → Nat
  | [] => 0
  | _ :: xs => length(xs) + 1

A proof by induction follows the same shape:

base case: []
step case: head :: tail
           + induction hypothesis for tail

This is not coincidence.

The inductive definition determines an eliminator/recursor—a principled way to consume values built by those constructors.

For data, that mechanism supports recursion.

For propositions about the data, it supports induction.

A useful slogan is:

same inductive structure
      ├── computation → recursion
      └── reasoning   → induction

19. What is a recursor?

“Recursor” sounds specialized. Start with the plain-English meaning:

An inductive type gives the theory a structured rule for consuming values built from its constructors.

That generated consumption principle is commonly called a recursor or eliminator.

Lean’s kernel does not need source-level pattern matching as a primitive core concept. The elaborator can translate pattern matching and structurally recursive definitions into lower-level recursor uses.

This is a major architectural idea: the user language can be expressive while the trusted logical core remains smaller.

20. Inductive propositions

Not every inductive type represents runtime data. An inductive type can live in Prop and represent evidence generated by logical rules.

Conceptually, imagine reachability in a graph:

reachable_refl:  Reachable(x, x)
reachable_step:  Edge(x, y) → Reachable(y, z) → Reachable(x, z)

A proof of Reachable(a, b) is then built from constructors corresponding to valid reasoning steps.

This gives logic the same constructor-based structure as ordinary data.

21. Inductive families: constructors can refine indices

A family such as:

Vector(A, n)

is not just one type. It is a family of types indexed by n.

Constructors can change/refine those indices.

Conceptually:

nil  : Vector(A, 0)
cons : A → Vector(A, n) → Vector(A, n + 1)

The type records facts about how construction changes length.

This enables proofs and programs where pattern matching refines what the checker knows about the index.

22. Why unrestricted nontermination is dangerous to logic

Suppose we allowed:

fakeProof : False

implemented as an infinite loop.

If the type system accepted that merely because the program never returned a wrong value, then False would appear inhabited and logical consistency would collapse.

A proof-oriented total fragment therefore cannot treat arbitrary nontermination as an ordinary proof-producing definition.

Lean elaborates accepted recursive functions into core constructions justified by structural or well-founded recursion, or uses distinct mechanisms for partial computation that do not silently become ordinary proofs.

The general lesson:

Termination is part of the logical trust story.

23. Universes: what type does Type have?

We saw:

42  : Nat
Nat : Type

Now ask:

Type : ?

A naive answer:

Type : Type

creates well-known logical paradoxes in sufficiently expressive systems.

So Lean uses a hierarchy of universes.

Conceptually:

Type 0 : Type 1
Type 1 : Type 2
Type 2 : Type 3
...

Lean’s exact notation is built around Sort u, with Prop = Sort 0 and Type u corresponding to higher sorts.

You do not need universe arithmetic for ordinary beginner programs, but the hierarchy explains how the language can let types themselves be terms without collapsing into Type : Type.

24. Prop is a special universe

Prop is not just another data type.

Lean-style Prop has properties chosen specifically for logical reasoning.

Proof irrelevance

If p and q are both proofs of the same proposition P, the logic does not computationally distinguish them in the ordinary way data values are distinguished.

Plain English:

What matters is that P is proved, not which proof object happened to establish it.

Runtime irrelevance / erasure

Proofs in Prop are generally not intended to become runtime data just because they were needed for checking.

This is essential for writing rich specifications without carrying huge proof objects through ordinary execution.

Impredicativity

Prop supports powerful quantification patterns over propositions. The technical term is impredicative.

You can learn the practical proof style before needing the metatheoretic details.

Restricted elimination

Because Prop is proof-irrelevant and intended for logic, not every proposition can be freely eliminated into arbitrary computational data in every way. These restrictions preserve the intended separation between proof evidence and runtime-relevant data.

Lean connection: the special logical status of Prop

Lean’s official reference specifies several important properties of propositions: proofs of the same proposition are definitionally interchangeable (proof irrelevance), propositions are erased from compiled runtime code, propositions support impredicative quantification, and elimination from propositions into data is restricted except in permitted cases.

These are not marketing descriptions invented for ProofScript; they are part of the Lean semantic foundation that ProofScript v0.1 targets.

Official background: Lean Language Reference — Propositions and Universes.

25. Quotients: reasoning modulo an equivalence relation

Sometimes two concrete representations should count as the same mathematical object.

Examples in mathematics include:

A quotient lets the theory reason about values modulo an equivalence relation without pretending the underlying representatives are definitionally identical.

Lean includes quotient mechanisms in its foundational theory. ProofScript inherits this semantic target from Lean rather than replacing it with a simplified “generic dependent type checker” story.

For most software developers, the key lesson is:

Equality in a theorem prover can be richer and more principled than host-language object identity.

26. Structures: named fields with types that can depend

Structures package fields.

In a dependent setting, later fields may depend on earlier fields.

Conceptually:

structure NonEmptyArray(A) {
  values : Array(A)
  proof  : 0 < values.size
}

Now a value packages both data and evidence.

This pattern is common in proof-oriented programming: make invalid states harder or impossible to construct by storing the invariant together with the data it constrains.

27. Subtypes: values satisfying a predicate

A subtype has the conceptual form:

{x : A // P(x)}

Read:

“Values x of type A for which proposition P(x) holds.”

It packages:

value : A
proof : P(value)

Fin(n) can be understood in this general spirit: a natural value plus evidence of a bound.

Subtypes are another bridge from general types to precise specifications.

28. Sigma types: dependent pairs

An ordinary pair has conceptually fixed component types:

A × B

A dependent pair allows the second type to depend on the first value:

Σ x: A, B(x)

Read:

“A pair whose first component is x: A and whose second component has type B(x).”

Existential proofs and dynamically sized dependent data often have this witness-plus-dependent-evidence shape.

29. Type classes: automated implicit evidence

Suppose many functions need an equality operation, ordering, serialization rule, or algebraic structure.

You could pass such operations explicitly everywhere.

Type classes let the elaborator synthesize suitable implicit values from registered instances.

A beginner-friendly model is:

explicit dictionary passing
        ↓
automated instance synthesis

But ProofScript preserves Lean’s typeclass semantics rather than TypeScript interfaces. Typeclasses participate in elaboration and can depend on types and values in ways ordinary erased structural interface checking does not.

30. Coercions: typed conversion, not “trust me” casting

In TypeScript:

value as T

can assert a static view that the compiler cannot prove from the expression itself.

A ProofScript coercion is instead a typed function/registration selected by elaboration. The resulting term must still type-check.

That difference matters in a proof-oriented language. Silent trust escapes would undermine the connection between source types and checked terms.

31. Elaboration: why friendly syntax does not need to live in the kernel

ProofScript and Lean let users write concise syntax:

The trusted core does not need all of those as primitive concepts.

Elaboration is the process of turning convenient user-facing syntax into a more explicit core term/declaration.

Plain-English pipeline:

friendly source
     ↓
fill in hidden information
resolve notation / type classes
translate patterns / recursion
construct explicit terms
     ↓
small core language

This separation is one of Lean’s major design strengths.

32. The kernel: small checker, large language

Lean’s official reference describes the trusted kernel as a small type checker for the core type theory. It does not perform general unification or tactic search; those happen before final kernel checking. Recursive definitions are elaborated to accepted core mechanisms.

That gives a valuable trust shape:

large convenient language
        ↓
parser / macros / elaboration / tactics
        ↓
explicit core term
        ↓
small strict checker

If a tactic is buggy but produces an invalid proof term, the kernel should reject it.

If an elaborator makes a mistake but produces an ill-typed core declaration, the kernel should reject it.

This does not make the entire frontend irrelevant—the frontend could still prove the wrong statement if source-to-core fidelity is wrong—but it sharply limits what must be trusted for logical validity of the elaborated proposition.

33. Proof terms make independent checking possible

Because proof evidence is represented explicitly enough to be checked against the core theory, another checker can replay the claim.

That is a major advantage of proof assistants such as Lean.

The idea is:

producer: sophisticated
- elaboration
- automation
- tactics
- search

consumer/checker: comparatively small
- is this explicit declaration valid?

ProofScript’s own assurance story should preserve this asymmetry: proof construction may be powerful, but validation should be understandable and independently reproducible where high assurance is required.

34. Type theory does not replace specifications

A powerful type system cannot guess what you care about.

This theorem:

Ordered(sort(xs))

may be perfectly valid and still insufficient as a sorting specification.

You probably also want:

Permutation(xs, sort(xs))

Why?

Because an empty list can be ordered while losing every element.

Formal verification shifts bugs upward:

implementation mistakes
      ↓ reduced by proof
specification mistakes
      ↑ become more important

The theorem is only as useful as the property it states.

35. Type theory does not replace compiler correctness

Suppose a ProofScript theorem is kernel-valid.

That establishes a statement about the checked logical program/model.

If the generated TypeScript backend mistranslates the function, the source proof does not magically fix the backend.

You need a separate relation:

checked source meaning
        ↕
TypeScript execution meaning

This is why ProofScript → Lean + TypeScript is a separate page.

Verified-compiler projects such as CompCert make this distinction explicit: source-level properties carry to executable behavior only when compiler semantic preservation has itself been established for the relevant pipeline boundary.

36. Why TypeScript developers should care

You do not need to formalize your whole application to benefit from this way of thinking.

Dependent type theory changes the kinds of questions you can ask at an interface:

Ordinary type question

Is this a number?

Stronger domain question

Is this a natural number?

Dependent question

Is this a valid index for this particular collection?

Proposition question

Is this output a permutation of the input?

Proof question

Can the checker verify that this implementation always satisfies that property?

That progression is useful even when you prove only the highest-value invariants.

37. A compact mental model

If you remember only one diagram, remember this:

VALUES
42 : Nat

TYPES AS TERMS
Nat : Type

DEPENDENT TYPES
(n: Nat) → Fin(n + 1)

PROPOSITIONS AS TYPES
P : Prop

PROOFS AS VALUES
p : P

IMPLICATION AS FUNCTION
P → Q

UNIVERSAL PROOF AS DEPENDENT FUNCTION
(x: A) → P(x)

INDUCTIVE TYPES
constructors → recursion / induction

ELABORATION
friendly syntax → explicit core

KERNEL
check explicit core term

That is the intellectual heart of ProofScript.

Sources

Next: How Proof Works →