Resource-safe programming — no use-after-free, no double-free, no garbage collector — delivered in syntax you already know.
AffineScript is a small, affine-typed core language that compiles to WebAssembly. What makes it unusual is not the core but how you write it: through faces — surface syntaxes shaped like languages you already use. You write in a familiar shape; the affine core checks it; and you get guarantees the familiar language could never give you — no use-after-free, no double-free, no leaks, no garbage collector, costs you can see — with nothing to migrate.
Most safe languages ask you to adopt a whole new language and its ecosystem. AffineScript asks you to adopt a surface and keep working the way you do. The faces are not a friendlier coat of paint on a hard language; they are the delivery mechanism. They are the product.
Early and experimental. This is v0.2: the architecture is settled, the
implementation and the metatheory are partial and still moving. It is suitable
for experimentation, teaching, and small sound components — not yet for
production. What is proven, what is implemented, and what is still prose are
stated plainly below and tracked in SOUNDNESS-LEDGER.adoc.
-
Affine ownership. Every resource has exactly one owner. Use-after-free and double-free are type errors caught before the program runs, not crashes discovered after it ships.
-
No garbage collector. Memory and resources are released deterministically. No GC, no pauses.
-
Visible cost. Resource usage is tracked in the types rather than hidden, so the price of a piece of code is something you can read.
-
One sound core, many surfaces. Every face elaborates to the same checked core, so the guarantees are identical whichever surface you write in.
A face is a surface syntax together with a desugaring into one canonical core AST. The load-bearing rule is that a face adds no semantics of its own: it is pure re-shaping, and every check happens in the core. Three things follow:
-
N faces cost one proof. Soundness is proven once, for the core. Adding a face cannot weaken safety, by construction.
-
Errors speak your dialect. A mistake written in the Python-shaped face is caught by the affine core but reported back in Python-shaped terms.
-
Adoption is per person. You pick up the face that looks like what you already write; the discipline arrives underneath it.
# RattleScript (Python-shaped)
buf = open_buffer()
write(buf, "hello")
close(buf) # 'buf' is consumed here
write(buf, "world") # error: 'buf' was already used up by close()
# — caught by the affine core, explained in the shape you wrote# install
$ <install command here>
# compile a face program to WebAssembly
$ <compiler invocation here> hello.rattle -o hello.wasm
# run it
$ <runner invocation here> hello.wasmA runnable example lives in examples/ once the toolchain lands.
AffineScript is one setting of a more general machine.
-
Anytype — the kernel. A graded type-checker that is parametric over a grade algebra (a semiring): the discipline is an input, not something hardwired. Turn the grade to
affine + costand you get AffineScript. Other settings — a privacy budget, a security lattice — would give other languages. AffineScript is one instance of the kernel, not the whole of it. -
SystemET — the theory. A layered calculus in which runtime, equality, resources, recursion, and effects are clean strata stacked in order, rather than tangled together.
-
The totality cut — the move that keeps checking decidable. Type-level equality is just normalise-and-compare, with no coercion machinery, and type-level programs are required to terminate. Every other kind of power is layered above equality, never woven into it. (Cores such as Haskell’s System FC instead carry heavy coercion machinery inside equality itself — the thing this design is built to avoid.)
-
Faces to core. Many surfaces, one core AST, one proof.
AffineScript is not trying to replace your language or win a community vote. The unit of adoption is a project: one person can pick up a face for one job without anyone else changing anything. It earns its place where the pain is acute and the cost of switching ecosystems is low:
-
Sandboxed game mods. Untrusted extensions that must not crash or corrupt the host — the same shape as the plugin-safety problem in safety-critical systems. A mod language rides on an existing engine, so there is no game ecosystem to rebuild.
-
WebAssembly edge functions. Untrusted code that must run safely and portably at the edge — which is also the compile target.
-
Privacy- and security-typed queries. Where the kernel’s non-affine settings already have real demand.
|
Note
|
This is a long game, and we would rather say so. The faces lower the cost of trying AffineScript to almost nothing, but they do not conjure libraries. Ecosystem cold-start — the thing that kills most new languages — is the real risk here, and it is not yet solved. |
Soundness is partially mechanised, and honestly tracked. An initial,
axiom-free, machine-checked result for code-generation preservation exists
(Coq/Rocq). A number of residuals remain open; they are recorded — not hidden — in SOUNDNESS-LEDGER.adoc, which states for each claim whether it is
mechanised or still argued in prose.
The ledger is the source of truth for what currently holds. This README deliberately does not duplicate its list, so the two can never drift apart.
The history is part of the design, so here it is straight.
-
v0.1 reached for safety and faces together on a core that was not sound enough, and hit the coherence cliff — the failure where equality machinery collapses under its own weight. It was archived, on purpose.
-
The lesson forked two ways: Panoply, an austere discipline lab where every claim is scoped and there are no faces; and Anytype / SystemET, the rebuilt foundation.
-
v0.2 — this — is "save faces": recover safety and faces, this time on a kernel built to carry them. The faces are the reward for getting the core right, not an ornament hung on it.
AffineScript is an assembly of existing ideas, and the ideas are good ones. A configurable, grade-indexed type discipline is a research lineage about a decade deep:
-
Quantitative Type Theory (Atkey; McBride), shipped in a usable language as Idris 2 (Brady).
-
Graded modal types and Granule (Orchard and colleagues) — a graded kernel parametric over a semiring, and Anytype’s nearest living relative.
-
Linear Haskell — a linear fragment bolted onto a fixed core.
-
Rust — the affine discipline welded as a single fixed setting, and the proof that it scales to millions of working programmers.
The contribution here is the combination — a dial-able kernel, faces, the totality cut, and a WebAssembly target — rather than any one ingredient.
-
Faces match syntax, not every habit. The affine rules still bite, in friendly clothing — you cannot alias mutably the way a garbage-collected language lets you.
-
The metatheory is partly prose; the ledger says exactly how much.
-
The dial covers the grade-and-usage axis of language design, not the whole space.
-
Ecosystem cold-start is unsolved and is the main risk to adoption.