ProofScript Programming Language

ProofScript

TypeScript-style programming, with mathematical proofs.

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

ProofScript is a standalone dependently typed programming and theorem-proving language designed to feel readable to TypeScript developers while targeting Lean-compatible logical semantics. You write programs, state mathematical properties about them, and ask the language to check proofs of those properties.

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

theorem incrementGreater(n: Nat):
    n < increment(n) := by {
  omega
}

Read this in English: increment takes a natural number n and returns n + 1. incrementGreater says: for every natural number n, the result of increment(n) is greater than n. The proof after := must establish that mathematical statement.

A program can therefore come with more than a return type:

program
+
property
+
proof

That is the central idea of ProofScript.

Syntax note: canonical ProofScript declarations use def. For familiar introductory code, top-level binderless const and ordinary function declarations are accepted as TypeScript-oriented aliases for the corresponding def. They do not introduce JavaScript declaration semantics.

What the first example means

If Lean or theorem-prover syntax is new to you, the punctuation is part of the lesson.

Syntax Read it as Meaning
n: Nat “n has type Nat” n is a mathematical natural number
: Nat after ) “returns Nat” the function result has type Nat
:= “is defined/provided as” supplies a definition body or proof body
n < increment(n) “n is less than increment of n” the proposition being proved
theorem “declare a proved proposition” names a proposition together with evidence
by “construct the proof using tactics” begins tactic-style proof construction
omega “solve the supported arithmetic proof” arithmetic proof automation whose result must still check

The most surprising symbol for a TypeScript developer is usually :=.

Why := instead of =?

ProofScript keeps three ideas visibly distinct:

:=   definition / provision        “is defined as”
=    propositional equality        “is mathematically equal to”
==   Boolean equality computation  “compute whether these are equal”

For example:

const n: Nat := {
  5
}

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

#eval n == 5

Read the three lines differently:

  1. n := 5 — define n as five.
  2. n = 5 — state a proposition that n equals five.
  3. n == 5 — compute a Boolean equality test.

The punctuation is not decoration. ProofScript keeps definition, logical equality, and executable equality separate because they have different meanings in the type theory.

How to read ProofScript code if you have never used a theorem prover

ProofScript deliberately looks familiar, but a few symbols have meanings that are more precise than their TypeScript look-alikes. Before going further, here is a small “decoder ring.”

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

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

Read the function in English

“Define a function named add. It receives two natural numbers, a and b, and returns a natural number. Its result is a + b.”

Piece by piece:

Code Read it as What it means
function add “define a function named add” TypeScript-oriented alias for an ordinary ProofScript def
(a: Nat, b: Nat) “a and b are natural numbers” : means “has type”
: Nat “the result is a natural number” declared result type
:= “is defined as” supplies the definition body
{ a + b } “return the value a + b” the body is an expression, not a JavaScript statement block

Read the theorem in English

“For every natural number n, prove that adding zero to n returns n.”

Piece by piece:

Code Read it as What it means
theorem addZero “declare a proved statement named addZero” a theorem is a checked declaration
(n: Nat) “for an arbitrary natural number n” the theorem is general, not one test case
add(n, 0) = n “add n and zero equals n” = creates a proposition
:= “the proof is provided as” provision again—not equality
by “construct the proof using tactics” begins tactic-style proof construction
simp “simplify using proved/definitionally valid rules” proof-producing automation

The important shift is that the expression after the theorem’s colon is not a return type like number. It is a mathematical statement:

add(n, 0) = n

In ProofScript, a mathematical proposition can itself be a type, and the theorem body must provide a value—a proof—of that type.

Beginner rule: whenever code looks unfamiliar, first ask “How would I say this sentence in English?” The formal terminology comes second.

From TypeScript types to mathematical specifications

TypeScript can express useful relationships about JavaScript programs. Its purpose is to statically type-check JavaScript, and its type system is intentionally shaped around JavaScript’s programming patterns. The official TypeScript documentation explicitly describes structural compatibility and also documents deliberate areas of unsoundness chosen for practical JavaScript compatibility.

ProofScript starts from a different question:

What if a type could describe not only the kind of a value, but a mathematical fact that must be true about that value?

Consider indexing.

TypeScript

function first(xs: number[]): number {
  return xs[0];
}

The type says the function receives an array of numbers and returns a number. It does not, by itself, make “the array is non-empty” part of the function’s mathematical interface.

ProofScript

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

Read this in English: “first receives an array of natural numbers and also receives evidence h that the array’s size is greater than zero. Under that assumption it returns a natural number.”

The unusual parameter is:

h: 0 < xs.size

0 < xs.size is not a Boolean flag. It is a proposition. In Lean-style dependent type theory, propositions are types, so h is a value whose type is the proposition 0 < xs.size. That value is a proof.

The idea is:

ordinary value:   xs : Array(Nat)
mathematical fact: h  : 0 < xs.size

This is the bridge from programming into proof.

A type may depend on a value

Ordinary generics let types depend on types. Dependent types go further: a type can mention an ordinary program value.

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

Read this as: “Given a natural number n, produce a natural number that is guaranteed to be less than n + 1.”

Fin(n + 1) is a bounded natural-number type. Its bound contains the input n, so the result type depends on the input value.

That single idea enables types such as:

Fin(xs.size)
Vector(A, n)
Matrix(A, rows, cols)

These can express relationships that ordinary non-dependent type systems usually leave to comments, runtime checks, tests, or conventions.

Read more in Type Theory.

Propositions are types; proofs are values

Suppose P is a proposition:

P : Prop

Read this as:

“P is a mathematical proposition.”

If p has type P:

p : P

then p is evidence that P holds—a proof of P.

This gives logical notation a programming interpretation.

P → Q

Read it first as a function type:

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

Then read it logically:

“If P, then Q.”

Likewise:

(x: A) → P(x)

means:

“Given any x of type A, produce a proof of P(x).”

Logically, that is universal quantification: for every x, P(x) holds.

This propositions-as-types viewpoint is one of the central ideas behind Lean and ProofScript. It lets the same type theory describe ordinary programs, mathematical statements, and proofs.

Read the full explanation in Type Theory and How Proof Works.

What can ProofScript prove about software?

The useful question is not “can ProofScript prove programs?” in the abstract. The useful question is:

Which property of which program, under which assumptions?

Examples include:

Bounds

0 ≤ index < xs.size

Round trips

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

Normalization

normalize(normalize(x)) = normalize(x)

Sorting

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

Both sorting properties matter. A function returning [] could satisfy orderedness while obviously failing to preserve the input elements.

Authorization

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

State-machine invariants

Invariant(state)
→
ValidTransition(state, next)
→
Invariant(next)

Formal verification becomes useful when the theorem captures a property that genuinely matters to the software.

Read practical case studies in Verified Software and Examples.

Why correctness matters in ordinary software

Formal proof is easiest to understand when the property is connected to a failure that engineers actually care about.

Money: prevent value from appearing or disappearing

Imagine a pure transfer function:

function transfer(from: Nat, to: Nat, amount: Nat): Balances := {
  ...
}

Tests can cover many examples, but a central accounting property is universal:

total balance after transfer = total balance before transfer

A ProofScript development can turn that into a theorem over the formal transfer model. The theorem does not say the database can never fail; it says the checked transformation preserves the stated conservation law.

Authorization: “allowed” must imply policy permission

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

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

In English: “Whenever the authorization function returns allowed, the formal policy says this user is permitted to perform this action.”

A regression that accidentally returns allowed in a forbidden case is no longer merely something we hope a test happens to cover: it conflicts with the theorem obligation.

Retry logic: repeating an operation should not duplicate its logical effect

A payment or message handler may be retried after a timeout. A useful property can be idempotence:

apply(request, apply(request, state))
=
apply(request, state)

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

That does not automatically prove a real payment provider is idempotent. It proves the property for the formal operation/model you connected to the theorem.

Parsers: valid output should satisfy an invariant

parse(text) = some(config)
→
ValidConfig(config)

In English: “If parsing succeeds, the produced configuration satisfies the validity rules.”

This is useful because parsers sit on trust boundaries: configuration, tokens, network messages, and file formats all convert untrusted bytes/text into trusted internal structures.

State machines: impossible transitions should remain impossible

For an order system, you may want to rule out transitions such as:

Cancelled → Shipped

unless a formally specified recovery process exists. A transition theorem can prove that every accepted transition preserves the state-machine invariant.

The recurring pattern is:

important failure mode
      ↓
precise property
      ↓
ProofScript proposition/type
      ↓
proof obligation
      ↓
checked evidence

ProofScript is valuable when the property is important enough that “we have tests for some cases” is weaker evidence than you want.

One source program, two inspectable views

For the supported compilation subset, ProofScript can produce both a Lean artifact and executable TypeScript:

program.ps
    │
    ├── program.lean   logical / independently checkable view
    └── program.ts     executable TypeScript view

The important word is correspondence.

ProofScript does not claim that the three files are textually identical. They may use different syntax, data representation, helper functions, and compilation machinery.

For a verified subset, “the same” means something more precise:

The selected source meaning and observable program behavior are preserved according to a stated semantic relation.

For a simple pure function, that may be summarized as:

corresponding input
      ↓
ProofScript computation
      ≈
Lean interpretation
      ≈
TypeScript observable result

The exact claim must name the supported subset and what counts as an observation. This follows the same general discipline used in verified-compiler work: compiler correctness is about semantic preservation, not source and target text looking alike.

Read ProofScript → Lean + TypeScript.

What a proof does—and does not—guarantee

A machine-checked proof can be extremely strong, but it proves its formal statement, not every informal intention surrounding a project.

Keep these questions separate:

Did the theorem check?
        ≠
Did we state the right theorem?
        ≠
Did generated TypeScript preserve the checked source meaning?
        ≠
Do external APIs, databases, browsers, Node.js, and deployment behave as modeled?

A kernel-valid theorem about a parser does not automatically prove your network stack. A proof of Ordered(sort(xs)) does not prove that sorting preserves the input unless permutation preservation is also stated. A correct source theorem does not by itself prove a compiler transformation; execution correspondence requires separate evidence.

This is not a weakness unique to ProofScript. It is what precise correctness claims look like.

Read Verified Software.

Why study the type theory even if you never prove an entire application?

Dependent type theory teaches a powerful progression:

broad type
   ↓
precise type
   ↓
value-dependent type
   ↓
proposition
   ↓
proof-carrying specification

For example:

number
Nat
Fin(10)
Fin(xs.size)
Sorted(xs)
proof : Sorted(xs)

Each step says more.

Even when you use proofs only for the highest-value invariants, learning this style changes how you think about interfaces, preconditions, state, data validity, and correctness.

Get started

Installation status — coming soon. The official stable ProofScript npm distribution is not yet generally available. A pre-release package may be discoverable, but this website does not treat it as the stable production release. The planned stable installation command is shown on the Download page for preview only and should be re-checked before publication or use.

You can already continue with the language and proof documentation:

Sources and intellectual background

ProofScript v0.1 targets Lean 4.33.1 semantics. The explanations on this site are especially informed by:

Next: Docs →