RCE language specification

Abstract. RCE is a small programming language whose programs mean one thing everywhere. A program is turned into a Form: a state machine given by its states, its events, a step function that maps a state and an event to a new state and an outcome, and the log of events. Every runtime that runs the Form must produce the same results bit for bit, and the rules that make this so are checked by machine.

Figure (informative). The pipeline from source to Form, log, emit targets and host. Source: docs/figures.

Three plain points:

1. Same answer on every target. Arithmetic, text, floats and concurrency have one defined meaning; there is no undefined behaviour.
2. Every program ends. Loops, recursion and iterators are bounded, so the step function always returns.
3. Memory is safe by construction. Ownership, second-class borrows, regions and linear handles rule out use-after-free and data races.

Tiny example (a counter that refuses to go negative):

state Counter
    n: i64 = 0
event Dec
step Counter on Dec
    check n > 0
    n -= 1

Reading map. Files are in spec/book/ and are meant to be read in order:

INDEX.md lists every file with its hash; READ-PROTOCOL.md says how an agent proves it read the spec. RCE-SPEC.md is all of these files joined into one, generated by rce-book build.

Status. Draft 0.7, 2026-10-13. Status: for review. Version 0.7 (C.15) is version 0.6 with size-scaled standard library method costs (C.6.4); it is the only semantic difference between them, and every other change since draft 0.6 is an erratum that applies to every version (C.15). Versions 0.5 and 0.6 are still accepted with their meaning unchanged. Version 0.5 (sections 2 to 10) is unchanged from draft 0.5 except for the version declaration of 2.7 and rules W-VER-1, W-MOD-3 and W-TRAIT-3 now listed in section 7. Version 0.6 (Appendix C) is new in this draft: it is what the reference checker and the Lean files enforce and prove, and it applies only to modules that declare it, so every valid 0.5 program is still accepted. The core is mechanized in Lean 4 (spec/lean/, section 8), a reference type and well-formedness checker (spec/checker/, rce-check) implements sections 4, 5 and 7 including the admission gate of 6.9 (examples, checks, comptime and constants are evaluated), spec/tree-sitter/ is a tree-sitter port of the grammar checked against the LALR(1) tables of section 3, and grammar-level random programs are checked by rce-fuzz (spec/checker/). The production compiler has not been built from this document yet. Changes made while mechanizing are listed in 9.1 to 9.4. Draft 0.4 follows the language review in spec/LANGUAGE-REVIEW.md; draft 0.5 applies the changes that review proposed and draft 0.4 deferred (9.4).

RCE is defined by this document. A program is a text; its meaning is a Form P = (S, E, δ, D, λ) (section 6). Runtimes, emitters, harnesses and editors are not part of the language: they are implementations, and an implementation conforms when it accepts exactly the programs this document accepts and gives each one the meaning this document gives it.

Document status. This specification is the only normative text. SURFACE.md (the native surface design) and FORM.md (the compiler notes) are informative: two normative texts with two grammars could disagree, and only one of them is checked by machine. Their programs must still be accepted by the reference checker. The Form signature is 6.1.

The normative grammar is section 3, and it is also the machine-readable one: rce-spec-check (in spec/checker/, Rust only) reads the EBNF of section 3 from book/03-syntax.md, builds its LALR(1) tables and fails on any shift/reduce or reduce/reduce conflict, then parses every program in spec/examples/ and requires every program in spec/examples/reject/ to be refused, by the LALR(1) tables, the Rust parser and the tree-sitter port alike, then runs rce-check over the same files (all examples together form one program and must be accepted; the 12 syntax rejects, the 48 programs in spec/examples/ill_typed/ and the 16 in spec/examples/inadmissible/ must be refused). Current result (draft 0.5): 0 conflicts (100 rules, 472 productions, 932 states); grammar 51/51 accepted, 12/12 refused; checker 51/51 accepted, 12/12 and 64/64 refused (16 of them only by W-INT-1, W-CT-1 or W-LEX-3). Until 2026-10-12 the same grammar was kept as spec/rce.lark and checked with Lark (0 conflicts, 533 rules in Lark's expansion); that file is retired. rce-fuzz N SEED generates random type-directed programs from the grammar's productions, with targeted near-misses. 100,000-program run (8 parts × 12,500, seeds 1001–1008, spec/fuzz/RESULTS.md, with the former Python generator and Lark): all 100,000 parsed by LALR(1), exactly one Earley parse each, all accepted by rce-check; 516,012/516,012 rule near-misses and 392,362/392,362 syntax near-misses refused; 0 failures. That run used the draft 0.4 generator. From draft 0.5 the generator also covers extern, arena bound, structural recursion, f32, lane-wise arrays, device regions, byte text, u64, select, linear structs, LOOP_LIMIT and iterators; a 1,000-program run (seed 2026) of it has 0 failures. The Rust generator, with the section-3 LALR(1) tables as a third parser: 1,000 programs (seed 7), 0 failures, tree-sitter and LALR(1) agree on all 4,977 syntax mutants.