The authored full-language draft.

Parts II–VI of the original design — the expression notation, capabilities, supervision, mailboxes, behavior blocks, fragments, stencils, derives, sealed tools, modules, build films, tests, FFI — with every section carrying the tier its author assigned it, so you can read the language whole and see exactly where the implementation stops. The later topology work is not on this page; it is documented separately in Direction and Core Part II.

What this page is

WallRiderLang exists as two documents. The design draft is the complete, deliberately ambitious statement of the language: 46 sections across six parts, written as one argument. The frozen core extract is the small subset the TRVM Forge toolchain has actually grounded, and it is what Part I of the spec publishes.

The reason to publish the draft rather than only the frozen part is that a language you cannot see whole cannot be criticized. The frozen extract tells you the four objects you can wire together today. It does not tell you what the four route textures are for, why the podium needs a stable tie-breaker, why coherence has to be hash-pinned, or why derives are stratified. Those decisions are the language. They are also the part most likely to be wrong, so they are the part most worth exposing.

Part I of the draft — the four reading laws, containers, identity, routes, walls, time — is already published in full as the language guide. This page picks up at Part II and runs to the end.

The three tiers

Every section of the draft carries one of three status marks. They are the author's own classification, not a retrospective guess.

Three sections are split, because the split is real:

• §22 fact union is Core; §22's distributed trust settlement is Proposed.
• §20's deterministic floor is Core; §20.7's podium is Experimental.
• §44 exclusions apply across all three tiers — they are permanent regardless of status.

The reality check

Four corrections the draft makes about itself, because a status word alone hides the interesting distinctions.

1 · "Grounded" splits in two

A construct can be IR-grounded — the intermediate representation and runtime handle it — while being surface-ungrounded: there is no way to write it in source, and no round trip through the text form. Most of the Core-tier process machinery is in exactly that position. The frozen extract is a statement about families, not about what you can type.

2 · The mailbox is not a sixth role

MailboxDecl is IR-grounded. The async texture ~~ has no structural edge declaration, because an async message does not settle within the period and therefore cannot be an ordinary edge. The playground rejects [mailbox:m] as source for that reason, and formatCore refuses to emit a role its own parser would reject.

3 · A world and a run of a world are different documents

Periods and [epoch:N] claims are run inputs. They belong to a scenario document, are outside the SemanticArtifactID, and are rejected inside world source with WRL_WORLD_SOURCE_HAS_SCENARIO. Editing the world moves the id; editing the scenario does not.

4 · Of the four textures, only one is surface-grounded

-- can be written, sealed and round-tripped. ~~, == and !! have frozen notation and frozen guarantees, and no writable surface construct. In particular == is not nearly done — a verified route needs a checker identity, a policy version and an evidence hash, none of which have a surface form.

Source: WallRiderLang — Complete Design Draft, status note and reality check, revised for Core 0.1.2.

10 · The punctuation rule Experimental

The expression notation is where ordinary computation lives: values, records, arithmetic, functions, pattern matching, collections. It appears inside state cells, route arguments, guards, behavior blocks, derives and tests. It is deliberately conventional — the visual symbols describe the architecture of computation, not arithmetic.

That is why WRL writes mul rather than *, and and rather than &&. Not aesthetics: * is already the wildcard and replication mark, and & is already graph composition. The sanctioned set is closed, and each entry records what it was audited against.

Nothing else. Operator overloading of punctuation does not exist, and is permanently excluded rather than deferred.

11 · Values and data types Experimental

Algebraic data types: records, variants, tuples, recursive data. There is no null.

type Rider = {
  name: Name,
  watts: Watts,
  energy: Energy,
  status: RiderStatus
}

enum RiderStatus {
  staged,
  riding(lap: Int32),
  dropped(reason: DropReason),
  finished(time: Period)
}

enum Option<T> { some(T), none }
enum Result<T, E> { ok(T), err(E) }

These are the foundation of messages, actor state, boundary responses, films and evidence. Absence is Option. Expected failure is Result. A genuine fault travels on !! — that three-way split is enforced statically and is the subject of §24.3.

Values are immutable; updating produces a new value:

let next = rider with { energy = rider.energy - cost }

12 · Bindings, functions, effect rows Experimental

12.1 · Bindings

let introduces an immutable binding. var permits local mutation as sugar; it lowers to immutable SSA form, so shared mutable variables are impossible by construction, not by convention.

let cost = grade_cost(course.grade)
var total = 0        ; local only; lowers to SSA

12.2 · Actors do not replace functions

Actors are for identity, concurrency, persistence and fault domains. Pure functions are for local calculation. A function declares its effect row with uses; an empty row means pure.

fn drain(rider: Rider, cost: Energy) -> Result<Rider, Exhausted>
  uses {} {
  let remaining = rider.energy - cost
  match remaining {
    e when e >= 0 => ok(rider with { energy = e })
    _             => err(exhausted(required=cost, available=rider.energy))
  }
}

A pure function has no hidden effects, is deterministic, is callable from guards and from metaprograms, and never requires spawning an actor. This is the answer to "everything is an actor" bloat: most computation is not concurrency.

12.3 · Effect rows are the type face of capability walls

fn download_world(id: WorldId) -> Result<Bytes, NetError>
  uses { net.send, storage.write }

A call whose row is non-empty can only execute where an actor's ports grant those capabilities. The checker proves the row. §21 is the runtime half of the same statement.

12.4 · Portability is a type property, not ceremony

Closures exist: riders.filter(fn(r) r.watts > 350).

A closure whose effect row is empty and whose captures are all content-addressed values has a canonical graph — it is a fragment, and may travel as a message, be stored, or be stamped. A closure capturing a live capability or an affine resource handle is not portable, and using it where a portable value is required is a compile error that names the offending capture.

The :: … // syntax of §30 is the literal notation for fragment values — the notation for the property, not its source. This is how "a copied fragment inherits no ambient authority" becomes a theorem rather than a rule.

13 · Pattern matching Experimental

match message {
  Command.attack(at=?p)                  => …
  Command.recover(amount=?n) when ?n > 0 => …
  _                                      => …
}

Graph patterns use the same binding system, so one mental model covers data and topology:

[rider:?id](energy=?e, status=riding(?lap))
  --when(?e < 20)-->
/feed-zone

Non-exhaustive matches over variants are static errors unless a _ arm exists.

14 · Generics and traits Experimental

14.1 · Generics are parametric

Never token templates. Const parameters where needed.

type Mailbox<T>        type Port<T>        type Graph<T>
type Fragment<T>       type Result<T, E>   type Vector<T, N: Int32>
fn map<T, U>(items: List<T>, f: fn(T) -> U) -> List<U>

Stencil parameters and type parameters are related but distinct; a stencil may take both — ::: cache<K, V>(name, capacity: Int32) … ///.

14.2 · Traits, and no class inheritance

trait Hashable {
  fn hash(self) -> Hash
}

trait Merge<T> {
  fn join(left: T, right: T) -> T
}

trait Verify<Candidate, Evidence> {
  fn verify(candidate: Candidate, evidence: Evidence)
    -> Result<Verified<Candidate>, Rejection>
}

Traits map directly onto runtime policies. Merge instances implement <~merge~>. Verify instances implement ==verified==> checkers. Boundary adapters are trait implementations. The abstraction mechanism of the expression notation and the policy mechanism of the process notation are the same mechanism.

14.3 · Coherence is hash-pinned Experimental

Instance resolution is a correctness property here, not a style preference. <~merge~> converges because every replica applies the same commutative, associative, idempotent join. If two replicas resolved Merge<FactSet<T>> to different instances, they would diverge while each believed it had merged correctly.

15 · Numerics and determinism classes Experimental

Int8  Int16  Int32  Int64      UInt8 … UInt64
Float32  Float64                Decimal
Fixed<Q>                        Duration   Period

Integer semantics are fully defined and identical on every target. Overflow is checked by default; wrapping_add, saturating_add and friends are explicit. Quotient truncates toward zero and remainder takes the dividend's sign, identically everywhere; div_euclid and rem_euclid variants exist. No numeric behavior may depend on build mode or platform.

Floating point is a determinism hazard and is treated as one. Identical executables on identical hardware reproduce float results; across hardware, compilers or optimization settings they do not — fused multiply-add, SIMD variation and transcendental library differences all break bit-equality. The answer is determinism classes bound to execution profiles.

The corresponding static check: a Float may not appear in a state cell of a world-profile actor. Duration is a wall-clock quantity and therefore effect-side; Period is logical time and replayable.

16 · Collections, strings, symbols Experimental

List<T>   Vector<T, N>   Map<K, V>   Set<T>   Bytes   String
Queue<T>  Mailbox<T>     FactSet<T>  Stream<T>

Every collection defines deterministic iteration order, canonical serialization, equality and hashing, and documented complexity. Nondeterministic map iteration does not exist — it is on the exclusion list, not the roadmap.

Data iteration is textual and never uses periods. The dot family means logical time and nothing else:

for rider in riders { … }
map(riders, score)
fold(results, initial, combine)

Four things other languages conflate are four different things here:

"rider a"      String — data
rider_a        identifier — a name in source
#rider-a       tag / content identity
@rider-a       address / stamp

Interned symbols exist as Symbol; the intern table is bounded per sealed scope and cannot grow without limit at runtime.

17 · Resources and ownership Experimental

The ownership model is small and sufficient: values are immutable; actor state is singly owned; messages are immutable; large binaries use shared immutable storage; external resources are affine handles; and capabilities cannot be duplicated unless their type permits it.

resource FileHandle
resource GpuBuffer
resource Socket

fn upload(buffer: borrow GpuBuffer) -> Result<Receipt, GpuError>
fn close(socket: move Socket)

A resource is consumed, moved, or explicitly borrowed. There are no shared mutable pointers anywhere in the language.

The five memory kinds (§18), the period cycle (§20.1–20.5) and the two invariants are covered in the guide. This part picks up the machinery built on top of them.

19 · Runtime entities Core

An implementation needs exactly six semantic entity types. Not five, not seven — this is the closed list.

20.6 · Boundaries are reduction operators Core

A wall is not decoration around a diagram. Each boundary is a reduction operator with a defined effect on memory.

A gate authorizes and externalizes; a commit freezes; a seal freezes and content-addresses. The finish line is literal: crossing //finish is the canonicalize-and-record reduction, which is why it can feed a podium directly.

20.7 · The podium Experimental

oN. consumes an eligible result set that has crossed a boundary this run and reduces it to a provenance-carrying object with N named places.

Podium {
  places: [r; N],        ; missing places are explicit _
  ranking_policy,
  evidence,
  source_boundary
}

//finish ==rank(by=time, tie=#id)==> o3.
[winner, second, third] <- o3.

The podium can rank anything, not only race results. o0. is accepted as sugar for o3. where the three-place reading is intended.

20.8–20.11 · Messages, schedules, determinism, quiescence Core

Messages are immutable facts

A ~~msg~~> in period t appends:

{ msg_id, sender, receiver, payload_hash,
  send_tag=(t,m), delivery_policy, provenance }

Delivery is a separate event. Under the default policy a message sent at (t, m) becomes deliverable no earlier than (t+1, 0). An actor cannot observe its own send within the same period, which keeps periods well-founded and forbids same-period causal loops. Exactly-once processing is not assumed; deduplication keys and acknowledgements are explicit.

Scheduled events

..after(periods=k)..> at period t creates an event due at t+k. ..after(5s)..> desugars through a /time wall that converts the duration into a period count; the observed conversion is a signed fact, so replay uses the recorded count and never a live clock.

The determinism property

The argument is short, and it is one clause per phase. OBSERVE canonicalizes external claims. ACCEPT creates missing receipts under pinned policies. MAP deterministically derives controls from newly accepted operations. COMMIT applies a canonically ordered compatible write set. REACT settles the same-period cascade by deterministic microsteps to fixpoint. FILM serializes every state variable and observation required to determine future behavior.

Nothing in that chain consults arrival order, wall-clock time, address identity, or iteration order over an unordered container. The write set is compatible because there is no destructive state conflict — only commutative appends and lattice joins — and it is canonically ordered because the ordering key is content, not schedule. The only entry point for nondeterminism is effect-wall observations, and those are captured in the film — so replay is exact.

Consequently "the same sealed film runs identically on desktop and console" is a testable property rather than a hope, provided the numeric rules of §15 are respected.

Termination is not quiescence

A graph is locally quiescent when no solid transition is enabled, no message is deliverable this period, no scheduled event is due, no actor is runnable, and all required boundary commits are complete. A distributed run is complete only under an explicit termination detector or a sealed finite-horizon film. Importing state that marks actors runnable invalidates a prior quiescence conclusion; restored work must be rescheduled before termination is declared.

21 · Effects, capabilities, entropy Experimental

All non-deterministic or external action crosses a named wall. No effect happens invisibly.

[request] --> /net
[frame]   --> /gpu
[sound]   --> /audio
[file]    --> /storage

An adapter returns a signed observation, and that is what enters the film — so a replay reproduces the run without repeating the call:

/net ==observed(response=#hash)==> [requester]

Capabilities live at boundaries and ports and are typed as the effect rows of §12.3. A copied fragment inherits no ambient authority; captured capabilities must be named:

[actor]{net.send}
[request] --> /net requires net.send

Effect walls are the only source of nondeterminism in the language. Everything else is a pure function of configuration content.

22 · Merging replicated facts Core (union law) Proposed (trust)

Monotonic knowledge merges as a CRDT join-semilattice. The merge is commutative, associative and idempotent; convergence follows from those laws alone.

[node:a] <~merge(facts)~> [node:b]
[node:a]{facts} + [node:b]{facts} --> [facts:joined]

<~merge~> canonicalizes both fact sets, unions them, and deterministically reduces. + is monotonic union, not arithmetic addition. The join function is a Merge<T> instance whose content hash is pinned into the program's canonical identity (§14.3) — so every replica of a given program hash provably applies the same join.

Semantic convergence is a separate concern from work efficiency; an implementation reports duplicate work, verifier work and divergence cost independently.

23 · Verification and sealing Core

A verified route requires evidence satisfying a named policy. The runtime does not infer what "verified" means. Verification is a protocol with an explicit checker identity — a Verify instance from §14.2 — a policy version, inputs, a result and an evidence hash.

[candidate]
  ==verified(by=proof, policy=forge.v1)==>
[film:#hash]

A failed verification travels on an explicit rejection route to a quarantine boundary — it does not silently vanish:

[candidate] !!reject(reason=?r)!!> /quarantine

Sealing (///) content-addresses the result, making it a reusable immutable artifact.

This is the section that explains why == is not nearly done. Four things have frozen meaning and no surface: the checker identity, the policy version, the evidence hash, and the rejection route.

24 · Supervision, faults, the error ladder Experimental

24.1 · Supervision

The caret denotes upward supervision or promotion:

[worker:a] ^ [supervisor:pool]

A supervisor deterministically chooses a policy in response to a fault — the response is a rule, not a callback:

[supervisor:pool](policy=restart_one)
  --on(crash(worker=?w))-->
@worker(id=?w, restored_from=last_checkpoint)

24.2 · Rest and wake

The underscore is a parked or quiescent actor state — observable, and therefore usable to define termination, snapshot safety and scheduler economics:

[worker:a] --> _
[queue] ~~job(?j)~~> [worker:a] _--> active(job=?j)

24.3 · The error ladder

Three levels, kept distinct, and the distinction is statically checked — this is the section most often skimmed and it is the one that does the work.

A missing file is err(file_not_found). A corrupted driver is [storage] !!crash(reason=corrupt_driver)!!> [supervisor]. A path that is a normal outcome must not silently become a fault; !! is reserved for faults and the checker rejects the promotion — in both directions.

25 · Mailboxes, streams, backpressure Experimental

Mailboxes are bounded by default. An unbounded mailbox is rejected unless an explicit policy says otherwise.

Mailbox<Job, capacity=1024, overflow=reject>

Backpressure is explicit demand signalling. Producers send only what consumers have demanded — there is no implicit flow control to reason about:

[consumer] ~~demand(32)~~> [producer]
[producer] ~~items(batch)~~> [consumer]

The stream vocabulary is Stream<T>, Subscription<T>, CancelToken, Demand. Cancellation is a normal message, observable in the film; a cancelled producer winds down through ordinary routes, not through faults.

26 · Actor behavior blocks Experimental

Routes are excellent for diagrams; complex actors also need an organized textual home. A behavior block declares an actor's state shape, ports and handlers in one place.

actor rider(name: Name, watts: Watts) {
  state (name=name, watts=watts, energy=100, status=staged)

  ports {
    radio: Mailbox<Command, capacity=64, overflow=reject>,
    road: Port<RideEvent>
  }

  on ~~Command.attack(at=?t)~~> {
    [self] --set(status=attacking(?t))--> (state)
  }

  on --tick--> when state.status = riding(?lap) {
    (state) <- try drain(state, 8)
  }

  on !!crash(?reason)!!> {
    [self] !!report(?reason)!!> [supervisor]
  }
}

The same actor, drawn. Every handler above is a route here, and the claim is that the two spellings are not merely similar but byte-identical after canonicalization:

profile forge.world.core.v1

[rider:self](name=name, watts=watts, energy=100, status=staged)
  {radio: Mailbox<Command, capacity=64, overflow=reject>, road: Port<RideEvent>}

[self] ~~Command.attack(at=?t)~~> [self].set(status=attacking(?t))
[self] --tick--> [self].drain(8) when status = riding(?lap)
[self] !!crash(?reason)!!> [supervisor]

27 · Evolution: migration and compatibility Experimental

27.1 · Live-state migration

Content-addressed modules evolve code: a new implementation is a new hash and names re-point. But a persistent actor in the world profile holds state typed by the old version, and re-pointing a name transforms nothing. Live state evolves through an explicit verified migration:

(state: Rider@#a91) ==migrate(policy=rider.upgrade.v1v2, by=#m7)==> (state: Rider@#b12)

A migration is a verified route: evidence-carrying, recorded in the film, orchestrated by supervisors (drain to _, migrate, wake), and replayable. A world upgrade is a sequence of migrations, not an improvisation.

27.2 · Message compatibility

Message types are content-addressed like everything else. A mailbox accepts the message hashes its port type declares; an unrecognized hash is a normal outcome, never a fault — which is what leaves room for explicit adapter routes between versions:

on ~~unknown(#msg)~~> {
  [self] --forward(#msg)--> /adapter.v1v2
}

Metaprogramming is a defining capability of the language, not an accessory — and it is not textual substitution.

28 · The three phases Proposed

The expression notation evaluates at three moments. It is the same language at each; the phase determines only what exists to be touched.

The build pipeline fixes when expansion happens: stencils expand, then derives evaluate to fixpoint, before canonicalization and hashing — and long before any reduction runs. Metaprograms cannot modify sealed artifacts; they produce new graphs, and therefore new hashes.

29 · The six laws of metaprogramming Proposed

; law 4, spelled
#[meta_fuel=10_000, max_nodes=50_000]

Laws 3, 4 and 6 are not ergonomics. They are the premises of the no-build property — without host-blindness there is no sound cache key, and without fuel there is no guarantee the key ever gets computed.

30 · Fragments Proposed

:: opens a quoted graph fragment; // closes it. A fragment is a first-class value of type Fragment<T> — data until stamped or explicitly executed. It supports typed holes, explicit captures, hygienic local identities, copying, transport as a message, signing, storage, inspection and canonical hashing.

:: breakaway(leader=?l, mate=?m)
  [rider:?l] ~~signal~~> [rider:?m]
  [rider:?l] --accelerate--> [road]
//

Free variables are illegal unless declared as holes; captured identities must be named:

:: with_clock(capture [shared:clock], hole ?target)
  [shared:clock] ~~tick~~> ?target
//

Copying a fragment mints fresh local identities unless an identity is explicitly marked shared. Because a fragment is a value, it travels as a message payload — code as a message:

[coach] --plan(::breakaway//)--> [team]

A fragment does not run merely because it exists. It must be stamped, executed, or crossed through an appropriate boundary. That is what makes "code can move" safe rather than alarming.

31 · Stencils Proposed

31.1 · The ordinary metaprogramming mechanism

::: opens a typed, hygienic graph constructor; /// seals it. Most things that are classes, component definitions, declarative macros, annotations, or infrastructure templates elsewhere are stencils here.

::: rider(name: Name, watts: Watts)
  : [rider:#name](
      watts=watts,
      energy=100,
      status=staged
    ){
      road: Port<RideEvent>,
      radio: Mailbox<Command, capacity=64, overflow=reject>
    }
///

Stamping instantiates: : @rider(a, 330). Idiomatic stencils scale from one actor to whole architectures — @supervised_pool(workers=8), @replicated_archive(nodes=3), @forge_pipeline(policy=world.v1).

31.2 · Identity derivation

Hygiene demands fresh identities per site. Incremental builds and stable diffs demand the same identities on every rebuild. Both hold via one normative formula:

#child = H( stencil#, canonical(args), path-within-expansion )

Same stencil, same arguments, same position ⇒ the same identity on every rebuild. Different site or arguments ⇒ a different identity. Colliding identities are caught at expansion, never at run time.

31.3 · The expansion pipeline

Stamping performs, deterministically: normalize arguments → allocate derived identities by the formula → substitute parameters → alpha-rename locals → validate capabilities and budget → canonicalize → attach provenance.

32 · Derives Proposed

Some transformations are inconvenient as stencils — cross-cutting rules like "every faultable actor gets a supervisor". Those are derives: expression-notation functions over typed graphs, evaluated at expansion time.

derive supervise_faulting(g: Graph<Actor>) -> Graph<Supervision> {
  for actor in g.actors
  where actor.can_fault and actor.supervisor = none
  emit actor ^ [supervisor:#actor.id]
}

Invocation stamps the derive over a fragment, like a stencil: @supervise_faulting(::workers//).

Three normative restrictions give derives their guarantees:

Anything genuinely non-monotonic — deletion, rewriting, arbitrary recursion — belongs to sealed tools. That is the principled boundary between the two levels, and it is why the stratified system can be trusted without a budget on trust.

33 · Sealed tools behind /compiler Proposed

Parsers, schema generators, GPU layout generators, binding generators, asset importers — procedural power that cannot live in the stratified system — run as sealed tools behind an explicit compiler capability wall.

[schema:#game] --> /compiler
/compiler ==generated(tool=#generator-hash)==> [bindings:#hash]

A sealed tool requires: a pinned tool hash; explicit input hashes; declared capabilities; CPU and memory budgets; deterministic output where possible; recorded provenance; and a sealed generated artifact.

34 · Reflection Proposed

Compile-time reflection over canonical structure is rich and free:

graph.actors      graph.routes       graph.boundaries
type.fields       fragment.holes     fragment.capabilities

Runtime reflection is capability-controlled. A mirror over an actor is a capability — {reflect: Capability<Mirror<Pool>>} — that must be granted like any other port. Unrestricted runtime reflection over private actor state does not exist.

35 · Modules and the no-build property Proposed

35.1 · Content-addressed modules

module race.timing@#a184

export { Time, FinishResult, rank_finish }

import trvm.facts@#91bc as facts
import forge.world@#33ae as world

Human-readable names and versions are metadata that point to immutable hashes:

race.timing@1.4 -> #a184

A locked build stores the hashes, not only the human versions. Upgrading never mutates a sealed artifact; it produces a new artifact with a new hash, and names re-point. Because downstream references are to hashes, nothing silently changes underneath a consumer — a consumer opts into a new version by re-pointing a name. Live actor state evolves separately, by migration.

35.2 · The no-build property

Incremental compilation, distributed build caches and perfect reuse across machines follow immediately. The hard problem of incremental build systems — knowing when a cached result is still valid — does not exist here, because validity is hash equality. This is the single strongest argument for paying the canonicalization cost.

36 · Build films Proposed

The build pipeline is itself a deterministic process with effects only at declared walls — so it is recorded as one. Every build emits a build film: which stencils expanded with which arguments, which derives fired, which trait instances were resolved and pinned, which sealed tools ran against which input hashes, and what was hashed.

wrl replay build.film

Consequences: any build reproduces bit-for-bit; provenance views (Law 5) are film queries; and "why does this node exist?" has the same kind of answer at compile time as at run time. One mechanism, both worlds.

37 · Testing and conformance monitoring Experimental

37.1 · Tests are first-class graph specifications

test "formatting does not affect identity" {
  hash(program_a) = hash(program_b)
}

property "fact join is commutative" {
  for all a, b: join(a, b) = join(b, a)
}

film_test "worker restart" {
  run scenario
  restore checkpoint
  expect same observables
}

37.2 · The language is simulation-native

Every prerequisite of deterministic simulation testing — a deterministic scheduler, virtualized time, randomness funnelled through recorded seeds, effects behind mockable walls — is a construction property of the language, not a retrofit. So the test runner explores adversity as ordinary execution:

check schedules=10_000
check partitions=100
check restores=100
check scores=all          ; systematically enumerate scored-branch choices

Exploration randomness enters through /entropy, so every failing exploration replays exactly from its film. Scheduler randomization, fault injection, partition simulation and restore testing are modes of the one deterministic machine rather than four separate tools.

37.3 · Film conformance monitoring

A film is a total record and a sealed specification is executable — so conformance is a diff. An implementation may continuously validate production films against a sealed specification film's invariants, closing the gap between the verified design and the running system: the model and the implementation are the same graph.

38 · Foreign functions Proposed

The FFI is boundary-based. Impure native calls cross a named wall and return observations:

[physics_request] --> /native.physics
/native.physics ==observed(result=#hash)==> [world]

Pure native functions may be imported as verified deterministic modules:

extern pure fn vec_dot(a: Vec3, b: Vec3) -> Fixed<16>
  from artifact #native-math-v3

Every extern pins the target ABI, the compiler/toolchain hash, the native artifact hash, the declared effects and the determinism class. An extern pure claiming bit-exact determinism is testable against that claim, and is rejected if the artifact's outputs vary across supported targets.

Canonicalization (§39) and the grammar (§42) are published in the reference tables and the guide. What follows are the four reference sections that state what a conforming implementation must refuse, offer, never and prove.

40 · Static checks Experimental

A conforming checker rejects all of the following. Each is a load-bearing invariant of some earlier section, restated as a refusal.

41 · Execution profiles Experimental

An implementation may offer restricted profiles that trade expressiveness for guarantees. A profile is not a compiler flag — it changes what the checker accepts.

43 · Seven worked examples

These seven span sports, distributed systems, fabrication, biology, machine-assisted patching and a versioned service. Together they exercise every construct in the language — which is exactly why none of them can be written today. Each carries a note saying which tiers it depends on.

43.1 · Criterium race

staging · stencils · periods · async · finish · podium

; a five-lap criterium with async team radio and a podium

::: rider(name, watts)
  [rider:#name](watts=watts, energy=100, lap=0, status=staged){road, radio, timing}
///

: @rider(a, 330)
: @rider(b, 295)
: @rider(c, 410)
: @rider(d, 305)
: [coach](plan=wait_then_attack)
: [clock](period=0)

{
  [coach] ~~radio~~> [rider:*]
  [rider:*] ~~draft~~> [rider:next]
  [clock] ..tick..> [rider:*]
}

(
  [clock](period=?t) --advance--> (clock period=?t+1)
  [rider:*](lap=?l, energy=?e) --ride(cost=8)--> (rider:* lap=?l+1, energy=?e-8)
  [coach](plan=wait_then_attack) --when(clock.period=4)--> (coach plan=sent)
  [coach] ~~attack~~> [rider:c]
).5

[rider:*] --sprint--> //finish
//finish ==rank(by=time, tie=#id)==> o3.
[winner, second, third] <- o3.
///race-result

Read the last three lines together. The finish line is a commit boundary, so crossing it is what makes a result rankable; the rank policy names a stable tie-breaker because a podium without one would not replay; and the seal content-addresses the outcome. Nothing here is a library function.

43.2 · Supervised worker pool

mailboxes · quiescence · faults · restart

::: worker(id)
  [worker:#id](status=idle, checkpoint=0){jobs: Mailbox<Job, capacity=256, overflow=reject>, supervisor}
///

: [supervisor:pool](policy=restart_one)
: @worker(a)
: @worker(b)
: @worker(c)
: [queue](jobs=[j1, j2, j3])

[worker:*] ^ [supervisor:pool]

[queue] ~~job(?j)~~> [worker:*]
[worker:*] _--> active(job=?j)
[worker:*] --perform(?j)--> (worker:* status=idle, checkpoint=?j)
[worker:*] --> _

[worker:b] !!crash(reason="bad input")!!> [supervisor:pool]

[supervisor:pool](policy=restart_one)
  --on(crash(worker=?w))-->
@worker(?w, restored_from=last_checkpoint)

[supervisor:pool] ==pool_quiescent==> //done

This is the example WRL is weakest against today, and the site says so elsewhere: there is no supervision floor, no writable mailbox, no runtime-spawnable process. The design is stated; the runtime is not there.

43.3 · Replicated fact lattice

CRDT merge · partition · convergence

: [node:a]{facts, peers}
: [node:b]{facts, peers}
: [node:c]{facts, peers}

[worker:a] ~~candidate(program=#p1, result=true)~~> [node:a]
[node:a] --verify(program=#p1)--> [fact:#f1]
[fact:#f1] ==accepted(by=node:a)==> [node:a]{facts+#f1}

[node:a] <~merge(facts)~> [node:b]
[node:b] <~merge(facts)~> [node:c]

/partition
[node:a] <~blocked~> [node:c]
[node:c] --derive(from=#f1)--> [fact:#f2]

/partition --open--> _
[node:a] <~merge(facts)~> [node:c]
[node:b] <~merge(facts)~> [node:c]

[node:a]{facts} ==same_hash==> [node:b]{facts}
[node:b]{facts} ==same_hash==> [node:c]{facts}
///converged

The partition is a boundary, not a failure mode bolted on for testing. Convergence is asserted as an ordinary verified route between two fact sets, which is only meaningful because the join instance is hash-pinned.

43.4 · Forge world fabrication

model wall · checks · verification · seal

: [brief](goal="coastal cycling city", players=64)
: [seed:#city17]

[brief] & [seed:#city17] --derive--> [world_spec]
[world_spec] --> /model
/model ==observed(candidate=#layout1)==> [layout:#layout1]

[layout:#layout1] --check_connectivity--> [report:roads]
[layout:#layout1] --check_spawn_safety--> [report:spawns]
[layout:#layout1] --check_budget--> [report:budget]

[layout:#layout1]
  & [report:roads] & [report:spawns] & [report:budget]
  ==verified(policy=forge.world.v1)==>
[film:#world17]

[film:#world17] --> /gpu
/gpu ==preview(frame=#preview17)==> [designer]
[designer] ~~approve~~> [film:#world17]
[film:#world17] ==seal==> ///world17

A generative model sits behind /model like any other effect adapter: it returns an observation, which is what the film records. Replaying this build does not re-run the model. That is the whole argument for putting generation behind a wall.

43.5 · Cell signaling

membranes · diffusion · decay

::: cell(id, kind)
  [cell:#id](kind=kind, active=false, energy=50){membrane, neighbors}
///

: @cell(a, sensor)
: @cell(b, relay)
: @cell(c, motor)
: [field](signal=0)

[field](signal=?s) --increase(10)--> (field signal=?s+10)
[field] ~~diffuse(level=?s)~~> [cell:a]

[cell:a](kind=sensor, active=false) --when(signal>5)--> (cell:a active=true)

[cell:a] ~~ligand(type=go)~~> /membrane:b
/membrane:b --bind(type=go)--> [cell:b]
[cell:b] ~~relay(type=go)~~> /membrane:c
/membrane:c --bind(type=go)--> [cell:c]
[cell:c] --contract--> (cell:c energy=energy-5)

([field] --decay(1)--> [field]).10

A membrane is a / wall. Binding is a solid transition through it. Nothing about this domain required new syntax — which is the claim the example exists to test.

43.6 · Proof-carrying patch

parallel lanes · verified acceptance · seal

: [issue:#217](failure="stale imported schedule")
: [repo:#trvm](revision=#a91)

[issue:#217] & [repo:#trvm] --> /model
/model ==observed(patch=#p44)==> [patch:#p44]

|| {
  [patch:#p44] --compile--> [report:compile]
  [patch:#p44] --property_tests--> [report:laws]
  [patch:#p44] --replay_battery--> [report:replay]
  [patch:#p44] --diff_scope--> [report:scope]
}

[patch:#p44]
  & [report:compile] & [report:laws] & [report:replay] & [report:scope]
  ==verified(policy=trvm.patch.v1)==>
[film:#accepted-p44]

[film:#accepted-p44] ==merge_candidate==> //review
[reviewer] ~~approve~~> //review
//review ==seal==> ///release-candidate

A machine proposes; four independent checks run in parallel lanes; a named policy decides; a human approval is an ordinary async message into a commit boundary. The acceptance is an artifact with a hash, so "who accepted this and on what evidence" is a query, not an archaeology project.

43.7 · Versioned telemetry ingest

expression notation · behavior block · backpressure · migration · test

module ingest@#b12

type Reading = { sensor: SensorId, value: Fixed<16>, at: Period }

enum IngestNote { out_of_range(sensor: SensorId), duplicate(sensor: SensorId) }

fn validate(r: Reading) -> Result<Reading, IngestNote>
  uses {} {
  match r.value {
    v when v >= 0 and v <= 5000 => ok(r)
    _                           => err(out_of_range(r.sensor))
  }
}

actor ingest(shard: ShardId) {
  state (stored=0, noted=0)

  ports {
    readings: Mailbox<Reading, capacity=1024, overflow=backpressure>,
    archive: Port<FactWrite>
  }

  on ~~Reading(?r)~~> {
    match try validate(?r) {
      ok(?v)  => [self] --store(?v)--> {facts + ?v}
      err(?e) => [self] --note(?e)--> (state noted=state.noted+1)
    }
  }

  on ~~unknown(#msg)~~> {
    [self] --forward(#msg)--> /adapter.v1v2     ; unknown messages are outcomes, not faults
  }
}

; demand-driven collection
[ingest:shard] ~~demand(32)~~> [sensor:*]
[sensor:*] ~~Reading(batch)~~> [ingest:shard]

; upgrading a live shard
(state: Ingest@#a91) ==migrate(policy=ingest.v1v2, by=#m7)==> (state: Ingest@#b12)

test "validation rejects out of range" {
  validate({sensor=s1, value=9000, at=0}) = err(out_of_range(s1))
}

check schedules=10_000

This is the example that shows both surfaces at once. The behavior block and the drawn routes below it are the same language; by conformance they must canonicalize to identical bytes. The migration line upgrades live state without touching the module hash that produced it.

44 · Exclusions Permanent

The following are permanently excluded. They are not future work. Each would break a stated principle, and the reason is given rather than assumed.

45 · Reserved and implementation-defined Proposed

Deliberately left open. A conforming implementation may specify these; the language does not fix them. Naming them is how the draft avoids pretending to have answers it does not have.

46 · Conformance Core

An implementation conforms if it satisfies the following observable properties. They double as a test matrix — which is the point: a conformance claim you cannot execute is a marketing claim.

Today's toolchain demonstrably satisfies formatting invariance and the identity half of build invariance; those are what the browser conformance corpus asserts on every change. The other twelve are properties of a runtime this repository documents but does not contain.

The language becomes real when one small set of reading laws — shape says what a thing is, texture says how it moves, colons introduce and slashes bound, marks for architecture and words for computation — accurately expresses a bike race, a supervised server, a replicated document, a generated world, a biological pathway, a proof-carrying patch and a versioned service, and all of them compile to one inspectable canonical graph whose build, execution and history are equally replayable.