One source program, three views—and a precise question: what does “the same program” mean?
Home · Docs · Type Theory · Proofs · Verified Software · ProofScript → Lean + TypeScript · Reference · Examples · Download
ProofScript’s most interesting software-assurance story begins after the source theorem checks.
You may write:
example.ps
and produce:
example.lean
example.ts
Those files do not need to look identical. They need a defined semantic relationship.
This page explains that relationship without pretending compiler correctness is automatic.
A beginner-friendly analogy is translation between mathematical notation and executable notation.
These can all describe the same arithmetic function:
f(x) = x + 1
function f(x: Nat): Nat := {
x + 1
}
def f (x : Nat) : Nat :=
x + 1
They do not have the same characters or parse tree. The important question is whether they denote the same selected computation/property under the correspondence relation.
That is the sense in which this page uses phrases such as semantic preservation and execution correspondence.
Lean itself separates rich source elaboration from its core expressions/declarations and kernel checking; ProofScript’s source-to-Lean story therefore has to preserve semantic content, not superficial syntax. Official background: Lean — Elaboration and Compilation and Lean — Terms.
function add(a: Nat, b: Nat): Nat := {
a + b
}
theorem addZero(n: Nat): add(n, 0) = n := by {
simp
}
“
addadds two natural numbers.addZerostates that adding zero to any natural number returns the original number, andsimpconstructs/checks a proof of that fact.”
The source contains two different kinds of content:
program definition
+
logical theorem about that definition
A corresponding Lean artifact may have the shape:
def add (a b : Nat) : Nat :=
a + b
theorem addZero (n : Nat) : add n 0 = n := by
simp
This is not textually the same program.
ProofScript uses parenthesized application and braces; Lean uses its own concrete syntax.
What matters is whether the generated Lean declaration represents the same intended definition and theorem under the pinned Lean semantic baseline.
The relevant comparison includes more than spelling:
A valid Lean proof of the wrong theorem is not enough.
An executable TypeScript artifact may look very different because proof-only information can be erased and mathematical values may need runtime representations.
A simplified illustrative shape might be:
export function add(a: NatRuntime, b: NatRuntime): NatRuntime {
return natAdd(a, b);
}
The exact emitted representation is an implementation detail and should be documented by the actual release.
What matters is not whether the TypeScript resembles the .ps source.
The question is:
Does the generated TypeScript produce the observable behavior required by the checked ProofScript semantics for the supported subset?
Do not collapse these into one word like “equivalent.”
Does the generated Lean theorem state the same proposition intended by the .ps theorem?
ProofScript theorem type
≈
Lean theorem type
Does the generated Lean definition represent the same source-level function/constant semantics?
ProofScript definition
≈
Lean definition
Does generated TypeScript implement the selected observable semantics of the source definition?
ProofScript evaluation
≈
TypeScript execution
These are distinct obligations.
Never interpret:
.ps ≈ .lean ≈ .ts
as:
same characters
same syntax tree
same variable names
same helper functions
same memory representation
same object identity
same execution time
Those properties are usually irrelevant to the intended correctness theorem.
Instead:
“Same” means preservation of the formally selected semantics and observations.
Verified-compiler research gives a useful vocabulary.
CompCert states compiler correctness in terms of observable behavior: when compilation succeeds, the generated target program must preserve the allowed behavior of the source according to formally defined semantics.
The general lesson for ProofScript is:
source semantics
↓ compiler
target semantics
needs a theorem, validator, certificate relation, or other explicit evidence—not wishful similarity.
A source-level theorem can transfer to executable code only when the compiler relation preserves the aspects of behavior that theorem talks about.
For a pure deterministic function, a useful observation may simply be its result.
Conceptually:
source input a
↓
f_ps(a) ⇓ b
corresponding target input encodeA(a)
↓
f_ts(encodeA(a)) ⇓ encodeB(b)
Read:
“If the ProofScript function evaluates to mathematical result
b, the generated TypeScript produces the corresponding runtime representation ofb.”
That is much more precise than “the files are the same.”
Nat is not automatically a JavaScript number.
So correspondence may need relations such as:
RepNat : Nat ↔ RuntimeNat
Likewise:
RepList(A)
RepOption(A)
RepStructure(S)
The target can use a different physical representation as long as the representation relation and operations preserve the required source semantics.
This is standard compiler thinking: semantic equivalence does not require identical representation.
Suppose the source computes with arbitrary natural numbers:
const huge: Nat := {
123456789012345678901234567890
}
If generated TypeScript naively used an IEEE-754 number in a way that lost integer precision, the output would not preserve Nat semantics for all values.
A trustworthy TypeScript profile must therefore do one of the following:
The wrong answer is silently changing Nat into JavaScript numeric semantics.
A proof parameter such as:
h : 0 < xs.size
may have no runtime representation in generated TypeScript.
That can be valid because proof terms in Prop are logically/runtime irrelevant under the source theory’s erasure rules.
But erasing proof data is sound only if runtime computation does not improperly depend on the identity/content of erased proofs.
So:
proof erased
must mean:
“The semantics justify that this evidence is not runtime-observable for the compiled computation.”
not:
“We deleted it because TypeScript does not want it.”
The strongest .ps ↔ .lean ↔ .ts claim should apply to a precisely named subset/profile.
That profile should define at least:
A language can be larger than its strongest verified execution subset.
That is normal and honest.
Suppose a valid ProofScript feature has no faithful implementation in the current verified TypeScript profile.
A correct compiler behavior is:
unsupported
not:
compile to something similar and hope
This follows a standard compiler-correctness principle: a compiler correctness theorem can be conditional on successful compilation. Refusing unsupported semantics is compatible with correctness.
A strong initial verified subset commonly focuses on:
Why?
Because equivalence can often be phrased as:
same mathematical input
→
same mathematical output
Effects can be added later with richer observation models.
For effectful code, return values may not be enough.
Imagine two programs both return Unit, but one sends a payment request twice.
They are obviously not equivalent for the application.
So an effectful observation model might include:
result
+
state transition
+
exception outcome
+
external trace
The exact model depends on the supported effect system.
“Same TypeScript behavior” is meaningless until these observations are defined.
Suppose source semantics distinguishes:
normal return
exception E
The TypeScript backend must preserve that distinction according to its profile.
If source Except(E, A) is compiled using thrown JavaScript exceptions, the relation must account for:
The source type name alone does not prove any of this.
For asynchronous code, equivalence may depend on whether you observe:
ProofScript should not promise general async equivalence without a specified model.
This is exactly why the strongest product message focuses on a defined verified subset rather than saying “all TypeScript output is proved.”
It is tempting to say:
“Lean accepted the output, therefore the ProofScript source is correct.”
That skips a step.
A buggy frontend could translate:
importantProperty
into a weaker theorem that is easy to prove.
Lean would correctly validate the generated theorem, but the source-to-Lean translation would be wrong.
So high assurance binds the exact source identity to the exact elaborated/generated theorem statement.
The meaning of a theorem depends on its definitions and imports.
If:
secure(x)
has one definition in one environment and a different definition elsewhere, a theorem name alone is not enough to identify what was proved.
A verification certificate should therefore bind relevant environment/module identities, toolchain versions, and assumptions.
A source hash can tell you:
“This certificate refers to these exact bytes.”
It does not tell you:
“The translation from those bytes is semantically correct.”
Hashes solve identity, not semantics.
A useful certificate combines artifact identity with actual checked relations/proofs/validation outcomes.
A strong ProofScript build certificate can bind at least:
source identity/hash
normalized/elaborated identity
Lean artifact identity
TypeScript artifact identity
exact theorem/declaration types
imports/environment identity
assumption/axiom manifest
ProofScript version
Lean baseline/toolchain version
correspondence profile/version
checker/validator outcomes
Do not interpret the list itself as proof. The certificate is a container for evidence and identities that can be independently checked.
A serious verifier should not collapse everything into:
verified: true/false
Useful distinctions include:
accepted
rejected
unsupported
resource_exhausted
implementation_error
Why?
A missing implementation feature is not evidence that the source theorem is false.
A timeout is not a semantic rejection.
A checker crash is not a proof failure.
Correct reporting is part of trustworthy verification.
Generated .lean can provide an inspectable artifact in an established proof ecosystem.
A high-assurance workflow can replay it with a pinned Lean toolchain.
This provides additional evidence that:
But Lean replay alone still does not prove source-to-Lean or TypeScript execution correspondence. It is one link in the chain.
Lean’s ecosystem values independent checker implementations because explicit proof terms/declarations make cross-checking possible.
The general assurance idea is:
same artifact/statement
↓
checker A accepts
checker B accepts
This can catch implementation-specific bugs.
It does not logically prove that no checker shares a bug. Diversity increases confidence rather than creating absolute certainty.
There are multiple legitimate ways to establish correspondence.
Prove once that a transformation preserves semantics for all supported inputs.
For each generated artifact, produce/check evidence that this particular translation satisfies the required relation.
The compiler emits a certificate/proof alongside the target, and a smaller validator checks it.
ProofScript can use different techniques at different boundaries as long as the website names the actual evidence.
Do not treat every technique as equivalent in trust assumptions.
A mature user experience can present:
example.ps
as the source of truth, while making both generated views inspectable.
Best for TypeScript-oriented programming and specifications.
Best for inspecting/checking the Lean-compatible logical artifact and using Lean’s proof ecosystem.
Best for JavaScript-ecosystem execution and integration.
The value is not that each file has the same syntax.
The value is that their relationships are explicit and checkable for the supported profile.
ProofScript:
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);
}
The desired relation is not:
all three strings match
It is conceptually:
for every source n,
if runtimeN represents n,
then TS increment(runtimeN)
represents ProofScript increment(n)
This is a relation between meanings.
Suppose source-level verification proves:
∀ n, n < increment(n)
And suppose compiler correspondence establishes:
TS_increment(runtime(n))
represents
increment(n)
Then, relative to the representation relation and runtime assumptions, the source theorem can justify the corresponding property of the generated TypeScript result.
This is the real reason compiler correctness matters: it lets source-level verification say something about code that actually runs.
CompCert explicitly describes this kind of consequence: if a source property holds and compilation preserves observable semantics, the compiled program inherits that property in the relevant sense.
A careful ProofScript build can be understood as:
human intent
↓ specification fidelity
.ps source
↓ elaboration/source-to-core fidelity
checked core proposition + program
↓ kernel validity
logical theorem
↓ Lean artifact correspondence/replay
.lean
↓ execution correspondence
.ts
↓ runtime / FFI / platform assumptions
actual execution
No single arrow should be silently replaced with “verified.”
The benefit of ProofScript is that these arrows can be made far more explicit than in ordinary application development.
Next: Language Reference →