Typical Computing

This document is provisional. It needs a full verification pass from a sufficiently capable language model and likely a full rewrite.

Proofs are a compile-time mechanism for expressing and verifying semantic invariants within a program. They allow the compiler to track facts about values and relationships that cannot be represented by ordinary types, while generating no runtime overhead.

Unlike refinement or dependent types, proofs do not require the compiler to understand or prove arbitrary logical propositions. A proof simply represents evidence that some condition has been established elsewhere in the program.

All proofs are erased during compilation.

Motivation

Traditional type systems describe the shape of data.

name is string
age is i32

However, many important program properties are semantic rather than structural.

Examples include:

These properties are usually represented through documentation, conventions, runtime assertions, or discipline. Proofs allow them to become part of the compiler's reasoning.

Defining proofs

A proof is declared using the proof keyword.

AdminRights is proof (
)

A proof has one establishment site by default. One source expression acts as the authority that introduces that proof; the expression may execute any number of times and establish the proof for any number of values.

HtmlSafe is proof (
)

When a proof legitimately requires multiple independent establishment sites, it is declared as a federated proof.

HtmlSafe is federated proof (
)

Establishing a non-federated proof at more than one source location produces a prominent compiler notice at every conflicting location. The proof is still established so that the program remains runnable. Propagating an existing proof does not count as establishing it again.

Establishment sites are counted by source provenance. Repeated execution, generic specialization, inlining, and generated copies that share one provenance origin do not create additional establishment sites.

Proofs may declare parameters.

StringVerified is proof (
	owner is User with AdminRights
)

These parameters describe the evidence carried by the proof.

Proof parameters exist only at compile time.

Attaching proofs to values

Any value may carry one or more proofs.

value is string with StringVerified(owner)

The underlying runtime representation is unchanged.

The proof exists only during compilation.

Functions establish proofs by returning values with attached proofs.

foo(owner is User with AdminRights) (
	return "value" with StringVerified(owner)
)

Consumers may require proofs.

bar(v is string with StringVerified) (
	console.log(v + " is verified")
)

Attempting to call bar without a matching proof produces a compile-time error.

Pure proofs

Some proofs represent permission or authorization rather than information attached to data.

These are expressed without an underlying runtime value.

Ticket is proof (
)

Functions may return proofs directly.

getTicket() (
	return Ticket()
)

Functions may require proofs.

enter(ticket is Ticket) (
	console.log("You're in")
)

Usage:

main() (
	ticket = getTicket()

	enter(ticket)
)

Generated code:

main() (
	enter()
)

The proof variable and parameter disappear entirely during compilation.

Pure proofs behave as though they are attached to an implicit zero-sized compile-time-only value.

Runtime behavior

Proofs never exist at runtime.

They introduce:

They are purely compile-time constructs.

The compiler removes every proof after semantic analysis.

Relationship proofs

Proof parameters allow proofs to describe relationships between values.

StringVerified is proof (
	owner is User with AdminRights
)

When attached:

value with StringVerified(owner)

the compiler records that this specific proof refers to that specific compile-time instance of owner.

The proof is not attached merely to the type User.

It references the compile-time identity of the particular value.

This allows the compiler to verify relationships between values without requiring runtime identity tracking.

Compile-time identities

Ambiguities: codex://threads/019fe3e1-80d9-7183-9c20-98ff0930536e

Whenever a proof references another value, the compiler internally associates that value with a symbolic compile-time identity.

Conceptually:

owner
	↓

Owner#17

The proof records:

StringVerified(Owner#17)

If another user exists:

Owner#42

then:

StringVerified(Owner#17)

and

StringVerified(Owner#42)

are distinct.

These symbolic identities never exist at runtime.

They are simply compiler metadata used during type checking.

Flow analysis

Proofs participate in normal control-flow analysis.

The compiler propagates proofs as values flow through the program.

Aliases preserve proofs.

a = value
b = a

Both variables carry identical proofs.

Functions propagate proofs according to their signatures.

Generic code preserves proof information automatically.

Proof parameters

Proof parameters may themselves require proofs.

StringVerified is proof (
	owner is User with AdminRights
)

This allows semantic relationships to be composed naturally.

Proof parameters may also be generic.

Examples:

Authenticated(user)

Authorized(user, resource)

WithinRange(min, max)

EscapedFor(Html)

OwnedBy(owner)

The compiler treats proof parameters as opaque compile-time values.

It does not attempt to understand their meaning.

Establishing proofs

Proofs are established explicitly.

return value with StringVerified(owner)

The compiler records the point where evidence enters the proof graph.

This enables tooling to determine:

The compiler may use this information when reviewing semantic changes introduced by automated tooling.

Consuming proofs

Functions may require proofs.

send(html is string with HtmlSafe)

Only values carrying the required proof satisfy the parameter.

The runtime representation remains identical.

Only compile-time evidence changes.

Multiple proofs

Values may carry multiple proofs.

value is string with HtmlSafe UserVisible Escaped

The compiler tracks each proof independently.

Proof preservation

Operations preserve proofs only when their semantics preserve the corresponding invariant.

For example:

verified = sanitize(raw)

may produce:

string with HtmlSafe

Whereas:

verified + raw

would ordinarily produce:

string

because the proof is no longer valid.

Proof preservation is determined by the signatures of operations rather than inferred from arbitrary program logic.

Design philosophy

Proofs deliberately avoid theorem proving.

The compiler never attempts to prove semantic properties.

Instead, it verifies that evidence flows consistently throughout the program.

The language does not ask:

Is this string actually HTML safe?

Instead it asks:

Has the program established the HtmlSafe proof before using the value where that proof is required?

This keeps the system understandable, predictable, and computationally inexpensive.

Relationship to the type system

Proofs extend ordinary types rather than replacing them.

A value consists of:

Examples:

string

string with HtmlSafe

string with StringVerified(owner)

User with AdminRights

The runtime representation is identical in every case.

Only compile-time semantics differ.

Typical use cases

Proofs are intended for representing semantic facts such as:

Any property that can be described as "this fact has already been established" is generally a good candidate for a proof.

Differences From declare

The declare word establishes compiler-internal invariants and where those invariants are applied to a lexical scope. Proofs are different, they're invariants that are user-defined and follow objects and data. Integrating the two would lead to confusion.

Summary

Proofs provide a lightweight mechanism for expressing semantic invariants that cannot be represented by ordinary types.

They:

Proofs allow developers to model what has been established, while allowing the compiler to verify that those established facts are used consistently throughout the program.