ProofScript Programming Language

ProofScript Docs

A handbook for TypeScript developers who are new to dependent types and theorem proving.

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

The goal of this page is not to teach every edge case of the language. It is to give you a coherent mental model, much like a language handbook: enough to read ordinary ProofScript, write small programs and theorems, and understand what the checker is doing.

Syntax note: def is the canonical ProofScript definition form. function and top-level binderless const are TypeScript-oriented aliases for ordinary def definitions. Local immutable binding remains let.

1. From TypeScript to ProofScript

If you already write TypeScript, this should look familiar:

function add(a: Nat, b: Nat): Nat := {
  a + b
}

Read this as: “Define a function named add. It receives a and b, both natural numbers, and returns a natural number. Its body is a + b.”

The surface resembles TypeScript, but several details deliberately do not mean what they mean in JavaScript.

Nat is not number

TypeScript’s number describes JavaScript’s numeric value domain. ProofScript’s Nat is the Lean-style mathematical natural-number type: 0, 1, 2, ... with arbitrary-precision mathematical semantics at the source level.

A backend may choose an efficient representation, but representation must not silently redefine the source type.

:= is not JavaScript assignment

:=

reads “is defined as” or “is provided as.” It supplies the right-hand side of a definition, field, or proof.

ProofScript keeps plain = for mathematical/propositional equality.

That is why this is meaningful:

const answer: Nat := {
  42
}

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

The first := defines answer. The = inside the theorem states a proposition. The second := provides the proof.

1A. A five-minute syntax primer

If you come from TypeScript, the fastest way to become comfortable with ProofScript is to learn a few symbols before learning any type theory.

: means “has type”

n : Nat

Read:

“n has type Nat.”

This is close to a TypeScript annotation:

const n: number = 5;

but the ProofScript type Nat has mathematical natural-number semantics rather than JavaScript number semantics.

:= means “is defined/provided as”

const n: Nat := {
  5
}

Read:

“Define n as five.”

ProofScript keeps this separate from mathematical equality.

= means “is propositionally equal to”

n = 5

Read:

“The proposition that n equals five.”

This expression has type Prop; it can be proved.

== means “compute Boolean equality”

n == 5

Read:

“Run the available Boolean equality test for n and 5.”

Its result is a Bool.

fun is the canonical lambda introducer

For an anonymous function, canonical ProofScript writes:

fun (x: Nat) => x + 1

Read:

“A function taking natural number x and producing x + 1.”

The TypeScript-shaped form:

(x: Nat) => x + 1

may be accepted as an ergonomic alias, but canonical formatting uses fun. Also keep => distinct from the function-type arrow →.

→ means function or implication

Nat → Nat

Read:

“A function from a natural number to a natural number.”

When the two sides are propositions:

P → Q

read:

“If P, then Q,”

or, in proof-as-program language:

“Given a proof of P, produce a proof of Q.”

by { ... } means “construct a proof”

theorem self(n: Nat): n = n := by {
  rfl
}

Read the whole declaration:

“For every natural number n, prove that n equals itself. Construct the proof using the following tactic script.”

You do not need to memorize formal logic vocabulary before continuing. Keep translating code into English.

2. Values and types

Start with the simplest judgment:

42 : Nat

Read:

“42 has type Nat.”

The colon : is a type ascription/judgment marker. TypeScript developers already see the same punctuation in declarations:

const n: number = 42;

ProofScript keeps the colon because it naturally reads as “has type.”

Top-level value:

const answer: Nat := {
  42
}

Canonical form:

def answer: Nat := {
  42
}

They mean the same ProofScript definition.

3. Foundational types

ProofScript intentionally keeps Lean’s foundational names rather than replacing them with TypeScript aliases.

Common examples:

ProofScript Informal meaning Do not confuse with
Nat arbitrary-precision natural numbers JS number
Int arbitrary-precision signed integers JS number
Bool computational true/false value Prop
String strings host representation details
Char character value arbitrary JS string
Unit one-value type exactly JS void
Empty no-constructor empty type merely TS never
Option(A) explicit optional value merely A | null
List(A) inductive list merely A[]
Array(A) array abstraction raw JS array identity
Fin(n) natural number < n with evidence plain bounded number
IO(A) Lean-style effectful computation yielding A merely Promise<A>

The similarities to TypeScript can help you learn; they do not erase semantic distinctions.

4. Functions

Ordinary function:

function square(n: Nat): Nat := {
  n * n
}

Canonical form:

def square(n: Nat): Nat := {
  n * n
}

Function type

Nat → Nat

Read:

“A function from Nat to Nat.”

The Unicode arrow → is canonical. -> may be accepted as an ASCII alias.

A multi-argument function ultimately corresponds to nested function types. Conceptually:

A → B → C

associates to the right:

A → (B → C)

Read it as: “Given an A, then a B, produce a C.”

5. Generic programming: types are themselves terms

In ProofScript’s underlying dependent type theory, types participate inside the term language.

Nat : Type

Read:

“Nat itself has type Type.”

That lets us abstract over a type:

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

Read this as: “For any implicit type A, if you give me a value x of type A, I return a value of the same type A.”

The braces:

{A: Type}

mean that A is an implicit binder. The elaborator can often infer it from how the function is used.

A TypeScript analogy is:

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

But the analogy stops at syntax and abstraction. ProofScript’s Type lives inside a dependent type theory and can participate in much stronger relationships than TypeScript generic parameters.

6. What makes a type dependent?

An ordinary function type has a result type independent of the particular input:

Nat → Nat

A dependent function type allows the result type to mention the input value:

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

Read:

“Given a natural number n, return a value whose type guarantees it is smaller than n + 1.”

The output type is:

Fin(n + 1)

and it literally contains n.

This is a dependent function type, formally a Pi type.

Fin(n)

Fin(n) represents a natural number together with evidence that it is less than n.

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

Read this as: “Given evidence that n is positive, return n - 1 as a valid index below n.”

The notation:

⟨n - 1, by omega⟩

constructs the bounded value together with the required proof.

This is where types stop being broad labels and start expressing exact relationships between values.

7. Bool and Prop are different

This distinction is foundational.

Bool

true : Bool
false : Bool

A Boolean is ordinary computational data. A program can inspect it.

Prop

2 + 2 = 4 : Prop

Read:

“The statement that two plus two equals four is a proposition.”

A proposition is a type of proofs.

If:

h : 2 + 2 = 4

then h is a proof of that proposition.

This is why:

=

and:

==

are not interchangeable.

x = y forms a proposition. x == y computes a Bool through Boolean equality machinery.

7A. Three everyday ways stronger types prevent bad states

Dependent types become less abstract when you ask what invalid values an API should refuse to represent.

Example 1: an index that is known to fit

Ordinary signature:

Array(A) × Nat → A

The Nat could be far beyond the end of the array.

Stronger conceptual signature:

(xs: Array(A)) → Fin(xs.size) → A

Read:

“Given an array xs, accept only an index known to be smaller than the size of that particular array.”

The second input type depends on the first input value.

Example 2: a non-empty collection

Instead of accepting an arbitrary list and documenting “must not be empty,” an API can take evidence:

(xs: List(A)) → xs ≠ [] → A

Read:

“Give me a list and a proof that it is not empty; I can then return an element under that precondition.”

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

Read:

“For each natural number n, return a value guaranteed to be below n + 1.”

TypeScript generics can relate types to other types. Dependent types can additionally relate types to ordinary values.

8. Your first theorem

theorem twoPlusTwo: 2 + 2 = 4 := by {
  rfl
}

In English

“Declare a theorem named twoPlusTwo. The theorem says 2 + 2 is equal to 4. Provide a proof by showing that the two sides compute to the same expression.”

Syntax

The theorem’s type is the guarantee. The theorem’s name is only a label.

9. Proof assumptions are ordinary parameters

theorem lessTransitive(
  a: Nat,
  b: Nat,
  c: Nat,
  hab: a < b,
  hbc: b < c
): a < c := by {
  omega
}

Read:

“For natural numbers a, b, and c, assuming a < b and b < c, prove a < c.”

The parameters:

hab: a < b
hbc: b < c

are proof values. This makes assumptions explicit in the function/theorem interface.

The theorem does not assert a < c unconditionally. It proves a conditional statement under the supplied assumptions.

10. Implication is a function type

Suppose:

P : Prop
Q : Prop

Then:

P → Q

can be read two ways.

Programming reading:

“A function that takes a proof of P and returns a proof of Q.”

Logical reading:

“If P, then Q.”

A proof can literally be a function:

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

intro h says: “assume the premise and name its proof h.”

exact h says: “the goal is exactly the proposition already proved by h; use it.”

Under propositions-as-types, ordinary function construction is implication proof construction.

11. Universal quantification is dependent function space

Consider:

(n: Nat) → P(n)

when P(n) is a proposition.

Read:

“For any natural number n, produce a proof of P(n).”

Logically this is:

∀ n: Nat, P(n)

∀ is pronounced “for all” or “for every.”

This is one reason dependent function types are so central: the same mechanism expresses both generic computation and universal mathematical claims.

12. Existential statements carry witnesses

∃ n: Nat, n > 10

Read:

“There exists a natural number n greater than ten.”

To prove an existential, you generally need:

witness
+
evidence that the witness satisfies the proposition

This constructive interpretation makes existence proofs computationally meaningful when the theory permits data extraction.

13. Equality: three different ideas

ProofScript distinguishes at least three notions that beginners often merge.

Definition/provision

:=

“is defined/provided as.”

Propositional equality

x = y

“x and y are equal” as a proposition that can have a proof.

Boolean equality

x == y

compute a Bool using the relevant Boolean equality instance.

There is also definitional equality, which is not merely another operator. It is the checker’s notion that two expressions count as the same because they reduce/unfold to the same core expression.

Example:

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

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

rfl works because double(2) computes/unfolds to the same value as 4 under the relevant definitions.

14. Inductive data

Inductive types define values by constructors.

A simple schematic shape:

inductive Color {
  | red;
  | green;
  | blue;
}

Read:

“A Color value is constructed by exactly one of the listed constructors.”

Inductive types are central because they support both:

programming: pattern matching + recursion
logic:       case analysis + induction

The same structure that tells you how data is built tells you how to consume it and how to prove properties about all possible values.

15. Pattern matching

For an option-like value:

def getOrZero(x: Option(Nat)): Nat := {
  match (x) {
    | none => 0
    | some n => n
  }
}

Read:

“If x is none, return zero. If it is some n, return n.”

The | symbol separates constructors/cases. => separates a matched pattern from the expression for that branch.

Pattern matching is not merely syntax sugar from JavaScript switch. In a dependent language, the type information available in a branch can become more precise because the branch tells the checker which constructor you have.

16. Recursion and termination

A proof-capable language must be careful with unrestricted recursion.

If every arbitrary nonterminating definition could inhabit every proposition, we could fake proofs by writing programs that never produce evidence.

So logical definitions accepted as total must satisfy the language’s termination discipline.

Structural recursion over an inductive value is the simplest case:

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

Read:

“The length of an empty list is zero. The length of a list with one head element and tail xs is one plus the length of the tail.”

The recursive call is on a structurally smaller list.

More advanced recursion can require an explicit well-founded argument.

17. Tactics

Tactics help construct proof terms.

They are not magical commands that make propositions true.

Common beginner tactics:

Tactic Plain-English meaning
rfl prove equality because both sides compute to the same thing
exact h use proof/value h because it exactly matches the goal
intro h assume the premise and name its proof h
assumption use a matching proof already in the local context
cases x consider every possible constructor of x
induction xs prove by the inductive structure of xs, receiving an induction hypothesis
rw [h] rewrite using equality h
simp simplify with proved/definitional rewrite rules while constructing proof evidence
omega solve supported arithmetic goals with a decision procedure
grind broader automated proof search using supported reasoning procedures

The important pipeline is:

tactic script
     ↓
constructed proof term
     ↓
kernel/type checker
     ↓
accepted or rejected

The proof checker, not the tactic’s confidence, decides whether the resulting proof term actually has the claimed type.

18. Type classes

Type classes let the elaborator synthesize implicit values that describe operations or evidence associated with a type.

A TypeScript developer can think of this first as automated dictionary passing.

Instead of manually passing an equality implementation everywhere, the typeclass system can search for the relevant instance.

The important distinction is that typeclass synthesis is an elaboration mechanism. It helps determine which values/instances fill implicit arguments; it does not add new kernel logic.

19. Coercions are not unchecked assertions

TypeScript has syntax such as:

value as SomeType

which can override the static type view without inserting a runtime conversion.

ProofScript coercions are conceptually different: a coercion is a registered, typed conversion mechanism selected during elaboration. The checker still validates the resulting term.

Do not mentally translate a ProofScript coercion into “trust me, treat this as another type.”

20. do, effects, and IO(A)

Pure logical terms are only part of programming. ProofScript also preserves Lean-style effectful programming concepts.

IO(A)

read:

“An effectful computation that, when executed in the IO model, can produce a value of type A.”

Do not equate this directly with JavaScript Promise<A>. A compiler may use promises or other runtime mechanisms, but the source semantics remain ProofScript/Lean semantics.

do { ... } provides structured monadic sequencing. The left arrow:

←

is read roughly as “run this computation and bind its result.”

ASCII <- may be accepted as an alias.

21. Contracts

ProofScript’s verification vocabulary can make common specifications more explicit.

def pred(n: Nat): Nat
  contract value {
    requires hPositive: 0 < n;
    ensures (result) => result < n := by {
      omega
    };
  }
:= {
  n - 1
}

In English

“pred receives a natural number n. The contract requires a proof that n is positive. The postcondition says the returned result must be smaller than n. The function body returns n - 1.”

Vocabulary

The critical design principle is:

Verification vocabulary does not create a second logic. Its meaning must lower to ordinary Lean-compatible terms, propositions, theorems, and proof obligations.

21A. Contracts as executable-documentation replacement—without becoming runtime-only checks

A common software pattern is a comment such as:

// amount must not exceed balance
// result is the remaining balance

Comments can be stale. A runtime assertion checks only executions that reach it. A ProofScript contract can instead generate logical obligations.

def withdraw(balance: Nat, amount: Nat): Nat
  contract value {
    requires enough: amount <= balance;
    ensures (result) => result + amount = balance := by {
      omega
    };
  }
:= {
  balance - amount
}

Read this in English

“withdraw receives a balance and amount. The contract applies when amount <= balance. Under that precondition, the returned result plus the withdrawn amount must equal the original balance.”

That is stronger than writing “should return the correct balance” because the postcondition says what “correct” means mathematically.

It is also narrower than saying “the banking system is correct.” The theorem does not automatically model concurrent transactions, persistence failures, currency conversion, database isolation, or an external payment processor.

22. A contract is not automatically an end-to-end runtime guarantee

Suppose you prove:

requires amount ≤ balance
ensures result = balance - amount

The theorem says something precise under its formal model.

It does not automatically prove:

This is why the site separates logical proof, software verification, and execution correspondence.

23. The verification workflow

A mature workflow can be understood as layers:

1. parse / elaborate source
2. check definitions and theorem terms
3. inspect theorem statements
4. inspect assumptions / axioms
5. bind source and generated Lean artifact
6. establish/check TypeScript correspondence for supported subset
7. record artifact/toolchain identity
8. run the actual software under explicit external assumptions

Each layer answers a different question.

24. Where to go next

If the syntax now feels readable, continue in this order:

  1. Type Theory — understand why the language can express these relationships.
  2. How Proof Works — understand how theorem checking works mechanically and logically.
  3. Verified Software — see which properties are valuable in real programs.
  4. ProofScript → Lean + TypeScript — understand what “same program” means for generated artifacts.
  5. Language Reference — consult exact forms and distinctions.

Sources

Next: Type Theory →