= AffineScript

[.lead]
Resource-safe programming -- no use-after-free, no double-free, no garbage
collector -- delivered in syntax you already know.

// TODO: status badges (build, license, version) once CI and a LICENSE file are in place.

== What this is

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.

== Status

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`.

== What you get

* *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.

== Faces

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.

.Illustrative -- schematic, not exact syntax
[source,python]
----
# 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
----

=== The roster

// TODO: confirm this roster against the repo and tag each face
//       as built / in progress / planned.
* *RattleScript* -- Python-shaped
* *JaffaScript* -- JavaScript-shaped
* *TortoiseScript* -- Logo-shaped (teaching)
* *CafeScripto* -- <shape>

== Quick start

// TODO: replace this block with the real toolchain commands.
[source,console]
----
# install
$ <install command here>

# compile a face program to WebAssembly
$ <compiler invocation here> hello.rattle -o hello.wasm

# run it
$ <runner invocation here> hello.wasm
----

A runnable example lives in `examples/` once the toolchain lands.

== How it works

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 + cost` and 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.

// TODO: link the SystemET / Anytype design notes once they have stable locations.

== Where this fits

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

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.

== Project history

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.

== Related work

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.

== Limitations

* 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.

== Documentation

// TODO: link the design notes and the examples directory once locations are stable.
* Soundness status: `SOUNDNESS-LEDGER.adoc`

== License

// TODO: state the license and add a LICENSE file.
