ProofScript Programming Language

ProofScript Examples

Programs, properties, proofs, and what each proof actually means.

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

These examples are ordered from ordinary programming toward stronger formal specifications.

Syntax note: def is canonical. function and top-level binderless const are aliases used in beginner-facing examples when they improve readability for TypeScript developers.

1. A top-level value

const answer: Nat := {
  42
}

In English

“Define answer to have type Nat, with value 42.”

New syntax

: — “has type.”
Nat — natural-number type.
:= — “is defined as.”

Canonical form:

def answer: Nat := {
  42
}

2. An ordinary function

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

In English

“Define add; it receives natural numbers a and b, and returns their sum as a natural number.”

Canonical form:

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

What is proved?

Nothing beyond type correctness yet. This is a program definition, not a theorem.

3. First equality theorem

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

In English

“Prove that the previously defined answer is mathematically equal to 42.”

Why `=` instead of `==`?

answer = 42 is a proposition.

answer == 42 would be a Boolean computation.

Why `rfl`?

answer unfolds to 42, so both sides are definitionally the same.

4. `:=`, `=`, and `==` together

const n: Nat := {
  5
}

theorem nIsFive: n = 5 := by {
  rfl
}

#eval n == 5

Read each line differently:

n := 5    define n
n = 5     proposition: n equals 5
n == 5    compute Boolean equality

This is one of the most important notation distinctions in the language.

5. Generic identity

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

In English

“For any inferred type A, take an A and return an A.”

What does `{A: Type}` mean?

It is an implicit type parameter. The elaborator can usually infer A from x.

TypeScript analogy

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

The generic intuition transfers; the underlying type theory is much richer.

6. A dependent result type

Type:

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

In English

“Given n, return a natural number smaller than n + 1.”

The output type literally contains the input.

That makes it a dependent function type.

7. Constructing `Fin(n)`

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

In English

“Given a positive n, return n - 1 as an index below n.”

Syntax

⟨value, proof⟩ constructs a value whose expected type requires both data and evidence.

by omega proves the arithmetic bound.

What is proved?

For the returned value, the bound required by Fin(n) is established.

What is not proved?

Nothing here says anything about a JavaScript array, memory safety, or external mutation.

8. Non-empty array access

def first(xs: Array(Nat), h: 0 < xs.size): Nat := {
  xs[0]
}

In English

“Read the first element of xs under a proof that xs has positive size.”

The precondition is represented as proof parameter h.

Software idea

A caller cannot obtain this function’s checked guarantee without satisfying the logical precondition.

9. Valid index as a value

Conceptual interface:

def get{A: Type}(xs: Array(A), i: Fin(xs.size)): A := {
  xs[i]
}

In English

“The index itself carries evidence that it is valid for the size of this array.”

This style moves the relationship into the argument type instead of a separate proof parameter.

10. Option pattern matching

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

In English

“If there is no number, return zero. If there is a number n, return it.”

Syntax

match (x) — inspect x by constructor.
| — start a case.
=> — branch result.

11. Recursive list length

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

In English

“Empty list length is zero. A non-empty list has one plus the length of its tail.”

Why this recursion is natural

The recursive call uses the structurally smaller tail xs.

12. Proof from an assumption

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

In English

“If h already proves P, use h as the proof of P.”

Lesson

A proof can be an ordinary value passed as an argument.

13. Implication

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

In English

“If P is true, then P is true.”

Programming interpretation

Construct a function from proof of P to proof of P.

14. Arithmetic theorem

theorem successorGreater(n: Nat): n < n + 1 := by {
  omega
}

In English

“Every natural number is smaller than its successor.”

Why this is stronger than tests

The variable n is arbitrary, so the theorem covers the entire Nat domain described by the statement—not a finite list of examples.

15. Rewriting with equality

theorem replaceEquals(a: Nat, b: Nat, h: a = b):
    a + 1 = b + 1 := by {
  rw [h]
}

In English

“If a = b, then replacing a by b preserves equality after adding one.”

rw [h] uses the equality proof to substitute equals for equals.

16. Simplification

theorem addZero(n: Nat): n + 0 = n := by {
  simp
}

In English

“Adding zero to any natural number returns that number.”

simp simplifies the goal using definitions and proved simplification rules while constructing evidence.

17. Case analysis over `Option`

theorem optionCases{A: Type}(x: Option(A)):
    x.isSome = true ∨ x = .none := by {
  cases x with
  | none =>
      exact Or.inr(rfl)
  | some a =>
      exact Or.inl(rfl)
}

In English

“Every option is either the some case described by isSome, or it is none.”

`∨`

P ∨ Q means “P or Q.”

`cases x`

Split the proof according to every constructor that could have produced x.

18. Inductive proof idea: append length

Desired theorem:

length(append(xs, ys)) = length(xs) + length(ys)

Proof strategy:

induct on xs

[]:
  simplify

x :: rest:
  unfold append/length
  use induction hypothesis for rest
  simplify

What the induction hypothesis means

In the recursive case, the proof receives evidence that the theorem already holds for the smaller tail rest.

This is how the inductive data structure supplies the logical proof structure.

19. Reverse twice

A classic list theorem:

reverse(reverse(xs)) = xs

This is stronger than checking a few lists.

A typical proof requires induction and helper lemmas about how reverse interacts with append.

Engineering lesson

Large proofs often become manageable by identifying reusable algebraic lemmas, just like large programs become manageable through good abstractions.

20. Normalization idempotence

theorem normalizeIdempotent(x: Config):
    normalize(normalize(x)) = normalize(x) := by {
  ...
}

In English

“Once a configuration is normalized, normalizing it again changes nothing.”

Good use cases

canonical forms;
configuration cleanup;
expression simplification;
cache keys.

Missing property

This does not say normalization preserves the intended meaning of x. That needs a separate theorem if important.

21. Encode/decode round trip

decode(encode(x)) = some(x)

In English

“Every valid value survives an encode-then-decode round trip.”

What is proved

Correctness for values generated from the modeled source domain.

What is not proved

Behavior on every malformed byte sequence.

22. Sorting correctness

Weak specification:

Ordered(sort(xs))

Better combined specification:

Ordered(sort(xs))
∧
Permutation(xs, sort(xs))

∧ means logical “and.”

In English

“The output is ordered and contains exactly the input elements up to permutation.”

Lesson

Proof does not rescue an incomplete specification.

23. Authorization soundness

authorize(user, action) = allowed
→
PolicyPermits(user, action)

In English

“Whenever executable authorization returns allowed, the declarative policy says the action is permitted.”

Missing counterpart

If you also want to ensure legitimate actions are not incorrectly denied, prove a completeness direction as well.

24. State invariant preservation

Invariant(s)
→
ValidTransition(s, s')
→
Invariant(s')

In English

“Starting from a valid state, every valid transition preserves the invariant.”

Combined with an initial-state theorem, induction over transition sequences can establish the invariant for all reachable modeled states.

25. Contract example

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

In English

“Assume n is positive. Return n - 1. Prove the returned value is smaller than n.”

Logical shape

requires becomes proof context/assumption according to the pure contract lowering.

ensures becomes an ordinary theorem/proof obligation about the result.

The verification vocabulary does not bypass the logical checker.

26. Vacuous contract warning

Imagine:

requires n < 0

with n: Nat.

The precondition is impossible.

A postcondition can be formally valid under that assumption and still tell you nothing useful about real calls.

A serious specification review therefore asks whether the precondition describes a reachable/meaningful domain.

27. Boolean/proposition bridge

Suppose you implement a Boolean check:

isSorted(xs) : Bool

and separately have proposition:

Sorted(xs) : Prop

A useful theorem is a bridge:

isSorted(xs) = true ↔ Sorted(xs)

↔ reads “if and only if.”

Why this matters

Now a fast executable Boolean computation is connected to the logical property by a checked theorem.

Without the bridge, a Boolean named isSorted is only a name and implementation.

28. Pure compiler correspondence example

ProofScript source:

function increment(n: Nat): Nat := {
  n + 1
}

Lean view:

def increment (n : Nat) : Nat :=
  n + 1

TypeScript view, simplified:

function increment(n: RuntimeNat): RuntimeNat {
  return runtimeNatAdd(n, runtimeNatOne);
}

Desired correspondence statement, conceptually:

if runtimeN represents n,
then TS_increment(runtimeN)
represents n + 1

Lesson

Correspondence is a theorem/relation about meanings, not a comparison of syntax.

29. Carrying a source theorem to TypeScript

Source theorem:

∀ n: Nat, n < increment(n)

Compiler correspondence:

RuntimeIncrement(rep(n)) = rep(increment(n))

Together, relative to the representation relation and runtime model, the executable result inherits the source property.

This is the deeper purpose of verified compilation.

30. What a verification certificate means

A certificate may bind:

source hash
Lean artifact hash
TypeScript artifact hash
theorem type
assumption manifest
toolchain versions
correspondence profile
validation outcomes

Important

The hashes identify the artifacts.

They do not by themselves prove semantic correspondence.

The proof/validator outcome is what supports the semantic claim.

31. A realistic verification summary

A useful report might read conceptually:

Source:             src/order.ps
Source identity:    <hash>
Logical status:     accepted
Theorem:            Order.preserveTotal
Assumptions:        approved baseline only
Lean replay:        accepted under pinned baseline
TypeScript profile: ps-ts-pure-v1
TS artifact:        <hash>
Correspondence:     accepted for profile
External boundary:  none in verified function

The exact product fields should follow the actual release format.

The important idea is that “verified” becomes inspectable evidence rather than a single unexplained badge.

32. Choosing what to prove

A practical hierarchy:

First prove invalid states impossible where easy

Use types such as:

Fin(n)
Option(A)
structured validated data

Then prove algebraic laws

idempotence
round trips
length relationships

Then prove domain invariants

authorization
state transitions
financial conservation
protocol safety

Then connect source semantics to runtime artifacts

That is where proofs start saying something strong about production execution rather than only an abstract model.

33. Inventory cannot go negative

Schematic model:

function applyEvent(state: Inventory, event: InventoryEvent): Inventory := {
  ...
}

theorem inventoryInvariant(
  state: Inventory,
  event: InventoryEvent,
  hValid: ValidInventory(state),
  hAccepted: Accepted(event, state)
): ValidInventory(applyEvent(state, event)) := by {
  ...
}

In English

“If inventory is valid before an accepted event, it remains valid afterward.”

If ValidInventory includes quantity >= 0 for every item, the theorem prevents an accepted transition from creating modeled negative stock.

Why this matters

The bug may require a sequence of reservations, cancellations, retries, and returns. An invariant theorem is not tied to one hand-written sequence.

What is not automatically proved

Warehouse hardware, concurrent database transactions, and external marketplace synchronization remain outside the theorem unless modeled and connected explicitly.

34. Money transfer conserves total balance

function transfer(state: Ledger, from: AccountId, to: AccountId, amount: Nat): Ledger := {
  ...
}

theorem transferConservesValue(
  state: Ledger,
  from: AccountId,
  to: AccountId,
  amount: Nat,
  hAllowed: CanTransfer(state, from, amount)
): TotalBalance(transfer(state, from, to, amount)) = TotalBalance(state) := by {
  ...
}

In English

“For every allowed modeled transfer, the total balance after the transfer equals the total balance before it.”

This is a conservation law. It is stronger than checking a few example transfers, but it does not by itself prove database atomicity or an external payment processor.

35. Retry idempotence

function applyRequest(req: Request, state: State): State := {
  ...
}

theorem retryIdempotent(req: Request, state: State):
    applyRequest(req, applyRequest(req, state)) =
    applyRequest(req, state) := by {
  ...
}

In English

“Applying the same request twice has the same modeled result as applying it once.”

Useful for retry-safe APIs, webhook consumers, provisioning, and job processing.

The theorem is about the modeled state transition. Exactly-once external side effects need additional correspondence/model assumptions.

36. Successful parsing implies valid data

function parseConfig(text: String): Option(Config) := {
  ...
}

theorem parsedConfigValid(text: String, config: Config):
    parseConfig(text) = .some(config) → ValidConfig(config) := by {
  ...
}

In English

“Whenever parsing succeeds with config, that configuration satisfies the formal validity predicate.”

This is different from a round-trip theorem. A good verified parser may need both.

37. Order state transitions preserve protocol rules

function transition(order: Order, event: OrderEvent): Order := {
  ...
}

theorem transitionSafe(
  order: Order,
  event: OrderEvent,
  hValid: ValidOrderState(order),
  hAccepted: EventAllowed(order, event)
): ValidOrderState(transition(order, event)) := by {
  ...
}

A rule inside ValidOrderState might encode:

Shipped(order) → Captured(order)

Read:

“Every shipped order must already satisfy the captured-payment condition in the formal model.”

38. Schema migration preserves validity

function migrate(old: SchemaV1): SchemaV2 := {
  ...
}

theorem migrationValid(old: SchemaV1):
    ValidV1(old) → ValidV2(migrate(old)) := by {
  ...
}

A stronger migration may also prove that a compatibility projection recovers the original information:

projectV1(migrate(old)) = old

when that is actually the intended semantics.

This is valuable because migration code can touch every stored record at once.

39. No accidental authorization allow

function authorize(user: User, resource: Resource, action: Action): Decision := {
  ...
}

theorem noUnauthorizedAllow(user: User, resource: Resource, action: Action):
    authorize(user, resource, action) = .allowed →
    PolicyPermits(user, resource, action) := by {
  ...
}

In English

“If the implementation says allowed, the formal policy must also say the action is permitted.”

This targets one of the highest-value classes of mistakes: an implementation branch that is more permissive than the policy.

40. Property composition: a stronger verified sorter

Instead of one oversized phrase such as “sort is correct,” use several theorems:

Ordered(sort(xs))
Permutation(xs, sort(xs))
List.length(sort(xs)) = List.length(xs)

If stability matters:

StableRelativeOrder(xs, sort(xs))

Each theorem says something precise. Together they characterize intended behavior more strongly than a single vague correctness label.

41. Why examples keep saying “what is not proved”

Formal verification rewards precise claims.

For every theorem, ask:

What exact proposition was checked?
What assumptions does it use?
Does the proposition characterize the behavior strongly enough?
Which runtime/environment boundaries remain outside the model?
If TypeScript is generated, what correspondence evidence connects it to the checked semantics?

The goal is not to weaken the value of proof. It is to make the value specific and trustworthy.

Further examples

For the theory behind these examples, see:

Next: Download →

ProofScript Programming Language

ProofScript Examples

1. A top-level value

In English

New syntax

2. An ordinary function

In English

What is proved?

3. First equality theorem

In English

Why = instead of ==?

Why rfl?

4. :=, =, and == together

5. Generic identity

In English

What does {A: Type} mean?

TypeScript analogy

6. A dependent result type

In English

7. Constructing Fin(n)

In English

Syntax

What is proved?

What is not proved?

8. Non-empty array access

In English

Software idea

9. Valid index as a value

In English

10. Option pattern matching

In English

Syntax

11. Recursive list length

In English

Why this recursion is natural

12. Proof from an assumption

In English

Lesson

13. Implication

In English

Programming interpretation

14. Arithmetic theorem

In English

Why this is stronger than tests

15. Rewriting with equality

In English

16. Simplification

In English

17. Case analysis over Option

In English

∨

cases x

18. Inductive proof idea: append length

What the induction hypothesis means

19. Reverse twice

Engineering lesson

20. Normalization idempotence

In English

Good use cases

Missing property

21. Encode/decode round trip

In English

What is proved

What is not proved

22. Sorting correctness

In English

Lesson

23. Authorization soundness

In English

Missing counterpart

24. State invariant preservation

In English

25. Contract example

In English

Logical shape

26. Vacuous contract warning

27. Boolean/proposition bridge

Why this matters

28. Pure compiler correspondence example

Lesson

Why `=` instead of `==`?

Why `rfl`?

4. `:=`, `=`, and `==` together

What does `{A: Type}` mean?

7. Constructing `Fin(n)`

17. Case analysis over `Option`

`∨`

`cases x`