ProofScript Programming Language

ProofScript Language Reference

Public reference for ProofScript v0.1. Semantic baseline: Lean 4.33.1.

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

How to use this reference

This page is precise reference material, but it should still be readable by someone new to theorem provers.

Each section tries to answer four questions:

What is the syntax?
How do I read it in English?
What does it mean semantically?
What is a small example?

If a term such as dependent function, inductive recursor, proof irrelevance, or elaboration is unfamiliar, use Type Theory for the long explanation and return here for the concise rule.

About Lean citations

ProofScript v0.1 is semantically pinned to Lean 4.33.1. Links below point to the official Lean documentation for the corresponding concept. The online /latest/ reference may describe a newer Lean release, so it is background/correspondence documentation rather than permission to silently change the ProofScript v0.1 baseline.

Canonical surface quick check

When writing standard ProofScript v0.1, prefer these canonical forms:

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

fun (x: Nat) => x + 1

def choose(p: Prop, h: Decidable(p), yes: Nat, no: Nat): Nat := {
  if (p) {
    yes
  } else {
    no
  }
}

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

The following are ergonomic aliases, not canonical formatter output:

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

const answer: Nat := {
  42
}

(x: Nat) => x + 1
Nat -> Nat

Key rules:

canonical lambda introducer: fun;
canonical function arrow: →;
canonical local immutable binding: let;
standard def/function/const := bodies use the mandatory outer { ... };
ordinary application uses f(x, y) but still elaborates to curried application;
match uses match (...) { | ... => ... }, with no branch-level terminator;
ordinary if uses ProofScript’s parenthesized/braced surface; Boolean-only conditionals use bif;
// is not a standard ProofScript line comment.

These rules follow the full v0.1 surface map and grammar; they are not JavaScript semantics.

1. Language identity

ProofScript is one semantic language with a TypeScript-oriented concrete syntax and Lean-compatible logical semantics.

The governing principle is:

Change the shape, never the concept.

ProofScript v0.1 targets Lean 4.33.1 semantics as its semantic compatibility baseline.

Official Lean background: The Lean Language Reference and The Type System.

Canonical source extension:

.ps

The language does not define a separate JavaScript/TypeScript semantic dialect inside .ps files.

2. Canonical syntax and TypeScript-oriented aliases

Canonical definitions use def:

def answer: Nat := {
  42
}

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

The parser may accept TypeScript-oriented aliases:

const answer: Nat := {
  42
}

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

They normalize to ordinary definitions:

const answer ...
→ def answer ...

function add ...
→ def add ...

function does not introduce JavaScript this, prototypes, constructor behavior, hoisting semantics, or function-object semantics.

Top-level const is an alias for a binderless definition. It is not the canonical local-binding form; local immutable bindings use let.

Normative v0.1 alias restrictions:

function is accepted only for a def written with one or more declaration binders.
const is accepted only for a top-level/module-level binderless def.
local const is not canonical ProofScript v0.1; use let.
both aliases expand to the corresponding braced def form before ordinary declaration elaboration.
canonical formatting prefers def.

3. Semantic punctuation

These distinctions are stable and important.

Syntax	Meaning
`:`	type ascription / “has type”
`:=`	definition, field, or proof provision
`=`	propositional equality
`==`	Boolean equality
`≠`	propositional inequality
`!=`	Boolean inequality
`→`	function/Pi arrow
`->`	ASCII alias for `→` where accepted
`∀`	universal quantifier
`forall`	textual alias for `∀` where accepted
`∃`	existential quantifier
`exists`	textual alias for `∃` where accepted
`fun`	canonical lambda introducer
`=>`	lambda / match-branch right-hand side
`\|`	constructor / alternative marker
`←`	monadic bind notation
`<-`	ASCII alias for `←` where accepted
`@[...]`	attribute syntax
`@f`	explicit application mode

Definition versus equality

def n: Nat := {
  5
}

:= means “define/provide.”

n = 5

= forms a proposition.

n == 5

== computes Boolean equality through the appropriate equality machinery.

4. Comments

Canonical comments follow Lean-style comment syntax.

Line comment:

-- comment

Block comment:

/- comment -/

Nested block comments are supported according to the Lean-compatible lexical rules.

// is not the canonical line-comment syntax because ProofScript preserves Lean syntax categories where // already has other meaning.

5. Identifiers and names

Identifiers name declarations, variables, namespaces, fields, constructors, and other entities.

Qualified names use namespace qualification according to Lean-compatible name-resolution rules.

The exact lexical categories, escaping, quoted identifiers, and parser-state behavior are governed by the full v0.1 reference.

6. Foundational types

ProofScript retains Lean terminology rather than replacing foundational types with TypeScript aliases.

Common canonical names include:

Prop
Sort u
Type
Type u
Nat
Int
UInt8
UInt16
UInt32
UInt64
USize
ISize
Float
Float32
Bool
Char
String
Unit
Empty

Parameterized source notation uses parentheses:

Option(A)
List(A)
Array(A)
Prod(A, B)
Sum(A, B)
Fin(n)
IO(A)
Task(A)
Except(E, A)
Decidable(P)

These names preserve ProofScript/Lean source semantics. A TypeScript runtime representation does not redefine the source type.

Examples:

const retries: Nat := {
  3
}

const delta: Int := {
  -5
}

const enabled: Bool := {
  true
}

const names: List(String) := {
  ["Ada", "Grace"]
}

Read:

Nat — natural numbers 0, 1, 2, ...;
Int — signed integers;
Bool — computational true/false data;
List(String) — a list whose elements are strings.

Official Lean background: Basic Types and The Type System.

7. `Prop`, `Sort`, and `Type`

Prop classifies propositions.

P : Prop

Sort u is the universe-level family used by the underlying type theory.

Type u denotes the corresponding data universe level above Sort u according to Lean semantics.

Ordinary code often uses simply:

Type

when explicit universe levels are unnecessary.

Universe-polymorphic definitions may declare universe parameters according to the full syntax.

Example:

universe u;

def identity{A: Type u}(x: A): A := {
  x
}

Read:

“For any type A living in universe u, identity returns a value of the same type it receives.”

Official Lean background: Universes and Functions.

8. Binders

Explicit binder:

(x: A)

Read: “explicit parameter x of type A.”

Implicit binder:

{A: Type}

The elaborator may infer the argument.

Instance-implicit binders use the typeclass/instance syntax defined by the language and participate in instance synthesis.

Binder information is semantically relevant to elaboration and is not merely formatting.

Example:

def firstOr{A: Type}(fallback: A, value: Option(A)): A := {
  match (value) {
  | .none => fallback
  | .some(x) => x
  }
}

{A: Type} is implicit: callers normally do not write the type argument when the elaborator can infer it from fallback or xs.

Conceptual call:

firstOr("none", names)

rather than forcing:

firstOr(String, "none", names)

Official Lean background: Function Types and Function Application.

9. Function types

Non-dependent function type:

A → B

Dependent function/Pi type:

(x: A) → B(x)

If the result does not actually depend on x, the dependent form reduces conceptually to an ordinary function type.

Function arrows associate to the right:

A → B → C

means:

A → (B → C)

Examples:

Nat → Nat

Read: “a function from Nat to Nat.”

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

Read: “given n, return a bounded natural below n + 1.” The result type depends on the input value, so this is a dependent function type.

Official Lean correspondence: Function Types, Function Application, and Theorem Proving in Lean 4 — Dependent Type Theory.

10. Function definitions

Canonical:

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

TypeScript-oriented alias:

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

A definition’s declared result type and body are elaborated under Lean-compatible typing rules.

Example with local computation:

function totalWithFee(base: Nat, fee: Nat): Nat := {
  let total := base + fee;
  total
}

Read:

“Define totalWithFee; compute a local value named total; return it.”

The outer { ... } is a ProofScript definition body. It does not introduce JavaScript’s arbitrary statement semantics.

A function with multiple parameters still has curried core function structure; parenthesized argument syntax does not introduce a distinct JavaScript tuple-call semantics.

11. Lambdas

Lean introduces function abstractions with the fun keyword. ProofScript keeps that concept introducer canonically.

Lean:

fun (x : Nat) => x + 1
fun (x : A) (y : B) => f x y
fun {A : Type} (x : A) => x

Canonical ProofScript:

fun (x: Nat) => x + 1
fun (x: A, y: B) => f(x, y)
fun {A: Type} (x: A) => x

Read the first example as: “Create an anonymous function that takes natural number x and produces x + 1.”

Optional TypeScript-oriented arrow-only alias

ProofScript v0.1 may also accept:

(x: Nat) => x + 1
(x: A, y: B) => f(x, y)

This is an alias, not the canonical lambda syntax. It normalizes to the corresponding fun form before semantic elaboration.

(x: Nat) => x + 1
        ↓ alias normalization
fun (x: Nat) => x + 1

Canonical formatting emits fun, just as canonical function types emit → rather than the ASCII alias ->.

Important distinctions

fun ... => ...

introduces a lambda/function abstraction.

A → B

is a function type.

=>

is the right-hand-side token used by lambdas and match branches; it is not the function-type arrow.

Multiple source binders still elaborate to nested curried functions. fun (x: A, y: B) => ... does not introduce JavaScript multi-argument function semantics.

Official Lean correspondence: The Type System and Function Application.

12. Function application

ProofScript uses parenthesized application syntax for common calls:

f(x)
f(x, y)

A multi-argument call lowers to ordinary nested application; comma syntax does not change currying semantics.

Example:

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

const six: Nat := {
  add3(1, 2, 3)
}

Although the source uses a familiar comma-separated call, its logical function structure remains the corresponding curried/dependent application structure.

Official Lean background: Function Application.

Explicit application mode:

@f(...)

exposes normally implicit parameters according to Lean-compatible application behavior.

13. Local definitions: `let`

Use let for local immutable bindings.

Conceptual form:

let x: Nat := 10;

let is a local definition mechanism, not the same thing as top-level alias const.

Its exact scoping/unfolding behavior follows the Lean-compatible semantics in v0.1.

Example:

function area(width: Nat, height: Nat): Nat := {
  let result := width * height;
  result
}

result exists only inside this definition body. Use let, not local const, for the canonical local immutable binding.

14. Local proof bindings: `have`

have introduces local evidence or an intermediate typed term, commonly in proof-oriented code.

Conceptually:

have h: P := by {
  ...
}

have and let have distinct elaboration/logical behavior and must not be collapsed merely because both introduce local names.

Example:

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

Read:

“We already have proof h of P; introduce the intermediate proof hAgain; use it to close the goal.”

15. Conditionals

ProofScript preserves Lean’s distinction between proposition-based if and Boolean-only bif, while reshaping the surface with parentheses and braces.

Ordinary `if`

Canonical ProofScript:

function max(a: Nat, b: Nat): Nat := {
  if (a <= b) {
    b
  } else {
    a
  }
}

Read this as: “If the proposition a <= b is decidably true, produce b; otherwise produce a.”

This remains a single expression. The checker synthesizes the required Decidable evidence for the proposition.

Boolean-only `bif`

When the condition is already a Bool, use the Boolean conditional concept:

def choose(b: Bool, yes: Nat, no: Nat): Nat := {
  bif (b) {
    yes
  } else {
    no
  }
}

if and bif are not aliases for JavaScript truthiness. ProofScript does not automatically treat 0, "", null, an object, or an arbitrary value as false/true.

Dependent if forms may bind proof evidence in the branch context according to the full language reference.

Official Lean correspondence: Conditionals.

16. Inductive types

Inductive declarations introduce constructors and generated elimination/recursion principles.

Simple shape:

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

Parameterized/indexed forms may depend on type and term parameters.

The semantic model includes Lean-compatible positivity, universe, constructor, recursor, and generated-equation behavior for supported forms.

Example with data:

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

Example with a parameter:

inductive Maybe(A: Type) {
  | none;
  | some(value: A);
}

An inductive declaration specifies how values can be constructed. The derived elimination/recursion principles then support both pattern matching/computation and proofs by cases/induction.

Official Lean background: Inductive Types.

17. Constructors

Constructors are introduced by an inductive declaration and may carry fields/arguments.

Conceptually:

inductive Box(A: Type) {
  | mk(value: A);
}

A constructor is not a JavaScript class constructor merely because it creates a value.

18. Pattern matching

ProofScript uses a brace-oriented match shape while retaining constructor alternatives.

match (x) {
| none => 0
| some n => n
}

| begins an alternative.

=> separates the pattern from its branch expression.

Pattern matching elaborates to the underlying inductive elimination machinery; it is not a new kernel primitive.

Dependent pattern matching may refine types according to the matched constructor.

Example:

def getOr{A: Type}(fallback: A, value: Option(A)): A := {
  match (value) {
  | .none => fallback
  | .some(x) => x
  }
}

Read:

“If value is empty, return fallback; if it contains x, return x.”

Official Lean background: Pattern Matching and Inductive Types.

19. Recursive definitions

Structurally recursive function example:

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

Recursive logical definitions must satisfy the accepted termination discipline.

Where structural recursion is insufficient, well-founded recursion and explicit termination evidence may be required.

Partial/unsafe computation has separate semantics and must not silently become ordinary proof-producing total definitions.

A second structural-recursion example:

def sum: List(Nat) → Nat
  | [] => 0
  | x :: xs => x + sum(xs)

The recursive call is on xs, the structurally smaller tail.

Lean background: recursive definitions with pattern matching are elaborated into lower-level recursor/well-founded constructions before kernel checking. See Elaboration and Compilation and Inductive Types.

20. Structures

Structures package named fields and may participate in dependent typing.

Conceptual shape:

structure User {
  id: Nat;
  name: String;
}

Structure syntax is not JavaScript object-literal semantics. Field types, constructors, projections, inheritance/extension behavior where supported, generated declarations, and universe behavior follow the ProofScript/Lean model.

Example value:

const ada: User := {
  { id := 1, name := "Ada" }
}

The inner { id := ..., name := ... } is structure construction with field provision. := again means “provide this field value,” not propositional equality.

Official Lean background: Structures and Constructors and Inductive Types.

21. Classes and instances

class introduces a typeclass declaration.

instance registers/supplies values for typeclass synthesis.

Typeclasses are not TypeScript interfaces. They participate in elaboration through implicit instance search.

Class parameters may include Lean-compatible outParam/semiOutParam behavior where supported.

Reference-aligned example:

class EqLike(A: Type) {
  eq(a: A, b: A): Bool;
}

instance: EqLike(Nat) := {
  eq(a: Nat, b: Nat) := a == b,
};

Read:

“EqLike(A) describes equality-like Boolean comparison for values of type A; the Nat instance supplies the checked instance value used by typeclass synthesis.”

This example follows the v0.1 Type Classes chapter directly. The instance is a definition-like declaration registered for synthesis; it is not a JavaScript class instance.

Official Lean background: Type Classes.

22. Coercions

Coercions are registered typed conversion mechanisms selected during elaboration.

Explicit coercion syntax may use:

↑x

A coercion must still produce a well-typed core term. It is not equivalent to an unchecked TypeScript type assertion.

In other words, the intended reading is closer to:

“Insert a known typed conversion here.”

not:

“Trust me; pretend this value already has the target type.”

Official Lean background: Coercions.

23. Propositions

A proposition has type:

Prop

Common logical forms include:

P → Q       implication
P ∧ Q       conjunction
P ∨ Q       disjunction
¬P          negation
P ↔ Q       logical equivalence
∀ x, P(x)   universal quantification
∃ x, P(x)   existential quantification
x = y       propositional equality
x ≠ y       propositional inequality

ASCII/textual aliases may be accepted where specified, but canonical logical meaning remains unchanged.

Examples with English readings:

P → Q

“If P, then Q,” or “given a proof of P, produce a proof of Q.”

P ∧ Q

“P and Q.”

∀ n, P(n)

“For every n, P(n) holds.”

∃ n, P(n)

“There exists an n for which P(n) holds.”

Official Lean background: Propositions and Basic Propositions.

24. `Bool` is not `Prop`

Bool is a computational data type.

true : Bool
false : Bool

Prop classifies propositions/proof types.

A Boolean test may be related to a proposition by a theorem/decidability mechanism, but ProofScript does not redefine every Boolean as a proposition.

Example distinction:

isEven(n) : Bool

may compute quickly, while:

Even(n) : Prop

states a logical property. A theorem can connect them:

isEven(n) = true ↔ Even(n)

Official Lean background: Propositions.

25. Equality

Propositional equality

x = y

has type Prop.

Boolean equality

x == y

computes a Bool using the relevant Boolean equality instance.

Definitional equality

Definitional equality is the core conversion relation used during type checking: expressions may count as the same because of allowed computation/unfolding rules.

It has no separate source operator analogous to ==.

Example:

function idNat(n: Nat): Nat := {
  n
}

theorem idNatLaw(n: Nat): idNat(n) = n := by {
  rfl
}

rfl succeeds because idNat(n) unfolds/computes to n; the two sides are definitionally equal before the equality proof is finalized.

Official Lean background: The Type System and Propositions and Proofs.

26. Theorems

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

A theorem introduces a named proposition and proof.

The theorem’s declared type is the proposition being established.

The proof body is elaborated to ordinary proof terms accepted by the logical checker.

A theorem with an assumption:

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

A theorem expressing implication:

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

Read the second theorem:

“For any proposition P, if you give me a proof of P, I can return a proof of P.”

Official Lean background: Theorem Proving in Lean 4 — Propositions and Proofs.

27. `opaque`, `axiom`, `abbrev`, `example`

ProofScript preserves distinct Lean declaration concepts rather than collapsing everything into one JavaScript-like declaration category.

opaque — an opaque definition/declaration with Lean-compatible reduction behavior.
axiom — introduces an assumed declaration without proof; downstream theorems inherit that assumption.
abbrev — reducible abbreviation semantics according to Lean.
example — checks a proposition/term without introducing an ordinary reusable theorem name in the same way.

These distinctions affect trust and elaboration and are not merely style choices.

28. Tactic proofs

Tactic proof block:

by {
  ...
}

Tactics construct terms/proof evidence.

Common tactics include:

rfl
exact
intro
apply
assumption
cases
induction
rw
simp
omega
grind

The availability and exact syntax of tactics depend on the imported environment and language baseline.

Tactic success does not bypass final logical checking.

Mini-example:

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

Read:

“Assuming a < b and b < c, prove a < c.”

Official Lean background: Tactic Proofs, The Simplifier, and grind.

29. `rfl`

rfl proves an equality when both sides are definitionally equal under the core conversion rules.

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

30. Rewriting

rw [h]

rewrites using an equality/iff theorem in the indicated direction according to the tactic rules.

Rewriting uses propositional evidence; it is not arbitrary textual substitution.

31. Simplification

simp

uses the simplifier and registered simplification lemmas/definitions to transform goals while constructing valid proof evidence.

The simplifier’s behavior depends on the active environment and simp set.

32. Arithmetic automation

omega

provides proof automation for its supported arithmetic fragment.

Automation is a proof-construction facility. The resulting theorem remains subject to the logical checker/trust model of the selected baseline.

33. `grind`

grind provides broader automated reasoning/search than simple rewriting/simplification.

Its exact behavior is part of the imported Lean-compatible tactic environment and must not be summarized as an untrusted “AI says true” mechanism.

34. Modules and imports

Module/import semantics follow the ProofScript v0.1 mapping to Lean-compatible environments.

Imports affect:

available declarations;
syntax/macros;
typeclass instances;
simplification lemmas;
attributes;
elaborator behavior;
theorem dependencies.

Therefore module/environment identity is part of high-assurance proof validation.

35. Namespaces and sections

ProofScript may use brace-oriented concrete syntax for namespace/section structure while preserving the corresponding Lean environment/scoping concepts.

They affect name resolution and declaration context; they are not JavaScript module blocks.

36. Attributes

Attributes use:

@[...]

They are Lean-style attributes, not TypeScript decorators.

Attributes can affect elaboration, simplification, typeclass registration, compiler behavior, and other environment extensions according to the specific attribute.

37. Notation, macros, and elaborators

ProofScript preserves a dynamic/extensible syntax model rather than pretending the full language is a fixed TypeScript grammar.

User-facing syntax can expand/elaborate into ordinary core terms/declarations.

A macro or elaborator must not create a new kernel logic merely because it adds new syntax.

The logical checker ultimately sees ordinary accepted core declarations.

Conceptual pipeline:

friendly/extensible source syntax
        ↓
macro expansion + elaboration
        ↓
explicit core expressions/declarations
        ↓
kernel checking

Official Lean background: Elaboration and Compilation, Terms, and Notations and Macros.

38. Monads and `do`

Canonical do syntax may use braces:

do {
  ...
}

Monadic bind notation:

x ← action

or ASCII alias:

x <- action

means “execute/bind according to the active monadic semantics.”

The source concept is Lean-compatible monadic sequencing, not JavaScript async/await identity.

Example shape:

def readLine: IO(String) := {
  do {
    let stdin ← IO.getStdin;
    let line ← stdin.getLine;
    return line;
  }
}

Read let line ← stdin.getLine as:

“Run this monadic/IO action and bind the produced value to line.”

Official Lean background: Functors, Monads and do-Notation and IO.

39. `IO(A)`

IO(A) represents an IO computation producing an A under the ProofScript/Lean model.

A TypeScript backend may implement relevant effects using JavaScript runtime facilities, but source semantics are not redefined as Promise<A> merely because a promise is used operationally.

External IO/FFI behavior introduces trust/model boundaries that must be documented for execution correspondence.

40. Verification extensions

ProofScript v0.1 includes verification-oriented vocabulary whose logical meaning must lower into existing Lean-compatible mechanisms.

Core vocabulary includes:

contract
requires
ensures
result
satisfies
assert
ghost
old
invariant

The principle is:

Borrow verification vocabulary, not verification semantics.

These constructs must not introduce a second weaker specification expression language or new kernel primitives.

Worked pure contract:

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

Read:

“pred may be specified under the assumption that n is positive, and the verifier requires a proof that the returned result is less than n.”

The verification vocabulary is ProofScript-specific surface material; the underlying propositions/proofs remain within the Lean-compatible logical foundation.

41. `requires`

Contract precondition:

requires h: P;

states proposition P as an assumption/proof obligation according to the selected contract lowering/model.

For pure value contracts, it can correspond to an ordinary proof parameter.

An impossible precondition can make a theorem vacuous, so satisfiability/usefulness remains a separate specification concern.

42. `ensures`

Postcondition shape:

ensures (result) => Q(result) := proof;

result names the returned value in the proposition.

The postcondition must be established through ordinary proof mechanisms. Failure does not justify inserting an axiom, sorry, or runtime-only assumption.

43. `satisfies`

satisfies associates a declaration with an explicit specification proposition/framework according to the normative v0.1 extension rules.

Its meaning must remain an ordinary checked logical obligation, not an unverified annotation.

44. `assert`

ProofScript’s verification-oriented assert form represents a proposition that must be established in the relevant pure/local verification context.

Do not conflate it automatically with JavaScript runtime console.assert or thrown runtime assertion behavior.

45. `old(...)`

old(e) refers to e in a formally defined entry/pre-state for a stateful verification model.

It does not imply an automatic snapshot of arbitrary JavaScript heap state.

A model must define which state is captured and how the theorem relates entry and exit states.

46. `ghost`

ghost introduces proof/specification-only information under the restrictions of the selected formal model.

Runtime erasure requires a justified non-interference discipline: erased specification data must not silently affect runtime-observable behavior in unsupported ways.

47. `invariant`

An invariant is a proposition that must hold at designated points such as loop entry/iterations or state transitions under the relevant verification framework.

A sound invariant workflow proves initialization and preservation, then uses the invariant to establish the desired postcondition.

48. Verification outcomes

A conforming implementation should distinguish semantic outcomes rather than collapsing all failures into one Boolean.

Core categories include:

accepted
rejected
unsupported
resource_exhausted
implementation_error

A timeout or missing feature is not evidence that a proposition is false.

49. Proof validation

A high-assurance verification result should bind, at minimum where applicable:

ProofScript source identity;
exact elaborated theorem statement;
referenced definitions/environment;
assumption/axiom manifest;
checker/toolchain version;
checker outcome;
generated artifact identity;
execution-correspondence evidence when such a claim is made.

Hashes establish identity, not semantic correctness by themselves.

50. Lean replay

Generated Lean artifacts may be replayed under the pinned Lean toolchain for independent cross-checking.

Lean acceptance establishes the validity of the generated Lean declarations under that environment. It does not by itself establish that the ProofScript frontend translated the intended source statement correctly or that generated TypeScript preserves execution semantics.

Those are separate correspondence claims.

This separation mirrors Lean’s own layered validation story: proof validity, assumptions, environment identity, and independent replay are distinct checks. Official background: Validating a Lean Proof.

51. TypeScript execution subset

ProofScript may define a subset/profile for which generated TypeScript carries stronger semantic-correspondence guarantees.

The profile must identify:

supported language forms;
source/runtime representation relation;
observable behavior;
effects/exceptions policy;
external assumptions;
evidence level.

Unsupported semantics should be rejected rather than silently weakened.

52. Trust summary

Keep four questions distinct:

logical kernel validity
source-to-core/source-to-Lean fidelity
environment/assumption identity
execution/compiler correspondence

A statement such as “verified” should be interpreted only with reference to the actual layers evidenced by the artifact/report.

53. Further reading

For explanation rather than terse reference:

External semantic background

Next: Examples →

ProofScript Programming Language

ProofScript Language Reference

How to use this reference

About Lean citations

Canonical surface quick check

1. Language identity

2. Canonical syntax and TypeScript-oriented aliases

3. Semantic punctuation

Definition versus equality

4. Comments

5. Identifiers and names

6. Foundational types

7. Prop, Sort, and Type

8. Binders

9. Function types

10. Function definitions

11. Lambdas

Optional TypeScript-oriented arrow-only alias

Important distinctions

12. Function application

13. Local definitions: let

14. Local proof bindings: have

15. Conditionals

Ordinary if

Boolean-only bif

16. Inductive types

17. Constructors

18. Pattern matching

19. Recursive definitions

20. Structures

21. Classes and instances

22. Coercions

23. Propositions

24. Bool is not Prop

25. Equality

Propositional equality

Boolean equality

Definitional equality

26. Theorems

27. opaque, axiom, abbrev, example

28. Tactic proofs

29. rfl

30. Rewriting

31. Simplification

32. Arithmetic automation

33. grind

34. Modules and imports

35. Namespaces and sections

36. Attributes

37. Notation, macros, and elaborators

38. Monads and do

39. IO(A)

40. Verification extensions

41. requires

42. ensures

43. satisfies

44. assert

45. old(...)

46. ghost

47. invariant

48. Verification outcomes

49. Proof validation

50. Lean replay

51. TypeScript execution subset

52. Trust summary

53. Further reading

External semantic background

7. `Prop`, `Sort`, and `Type`

13. Local definitions: `let`

14. Local proof bindings: `have`

Ordinary `if`

Boolean-only `bif`

24. `Bool` is not `Prop`

27. `opaque`, `axiom`, `abbrev`, `example`

29. `rfl`

33. `grind`

38. Monads and `do`

39. `IO(A)`

41. `requires`

42. `ensures`

43. `satisfies`

44. `assert`

45. `old(...)`

46. `ghost`

47. `invariant`