RCE: frequently asked questions

RCE is a programming language in which every program has one shape, called a Form, and code in other languages is generated from it [C1]. A Form is a tuple P = (S, E, δ, D, λ):

• S, the state the program holds, for example the balance of an account;
• E, the events it can receive, for example a deposit or a withdrawal;
• δ (delta), the transition: a pure, total and deterministic function that takes a state and an event to the next state and the outputs of that step;
• D, the durable log: every step recorded in a hash chain, each entry carrying the SHA-256 of the state it produced and of the entry before it;
• λ (lambda), the output map: what the program emits for a state and an event.

One state and one event give exactly one next state, and the state at any time is the fold of δ over the log, so every run can be replayed and checked bit for bit [C1]. Four public pieces make up the language today: the written specification, draft 0.9 [C2]; a reference checker, rce, that admits a program or names the rule it breaks; emitters that print an admitted program as Rust, Python, JavaScript or Scala; and proofs of the language's theorems in Lean 4 [C1].

It reports that the code requires change and names the rule the code breaks. Given a line that puts an assignment inside an expression, the checker at public main prints requires change FILE: line 1: W-SYN-1 expected `)` (found `=`) [C2]. Nothing runs until the code is changed. A module that uses a name it does not declare requires change by rule W-NAME-1; a construct the checker does not implement yet requires change by rule W-RES-1 [C1].

A program that is in Form can still receive an event that does not apply in its current state, such as a decrement of a counter that is at zero. That step keeps the state: theorem T8 (atomicity) states, and its Lean proof shows, that the state is unchanged, and the step is recorded in the log with the error it names [C1]. rce run prints such a step as kept: Underflow [C2].

rce emit, given a target and a file, prints the Form itself as one line of canonical JSON, or a self-contained program in Rust, Python, JavaScript or Scala [C2]. Every emitted program must print the reference trace of every example program byte for byte. For the Rust emitter, agreement with the reference evaluator is proved on a core of the language as a verified translation into MiniRust, a model of the emitted Rust; that the Rust compiler implements MiniRust is trusted and tested. For the Python, JavaScript and Scala emitters the agreement is differential testing on stated inputs, which says nothing about inputs outside the tested set [C1].

Every target keeps one behaviour at every numeric edge: integer division truncates toward zero (−7 / 2 = −3), the remainder takes the sign of the dividend, overflow and division by zero trap, and floating-point numbers are IEEE 754 binary64, rounded once per operator [C1].

The specification states its theorems and records the level of each one exactly: proved about the core semantics, proved on a semantics of a core, proved about a separate model, checked by test vectors, or tested. Proved about the core are, among others, determinism (theorem T1), totality with an explicit bound on evaluation steps (theorem T2), replay of the log (theorem T3), independence of the log hashes from names (theorem T7) and atomicity (theorem T8). At public commit f2bd7222 the Lean audit reads 5,052 theorems that use only the standard axioms, with no unfinished proof [C1].

What is not proved: nothing yet connects the Lean semantics to the Rust checker that a reader runs, and the conformance report for the mechanised core records 210 tests passing, 1 failing and 1,766 unsupported of 1,977, so about a tenth of the suite is under the theorems [C1]. A proof about a model is not a proof about the program.

A research proposal, not a built system [C3]. It asks whether a model of the JEPA kind could propose Forms from a stated intent while the RCE checker alone decides what is admitted, so that nothing depends on the model being right. It states thirteen hypotheses, H1 to H13, five falsifiers, RJ-F1 to RJ-F5, and a programme in phases. No such model has been built, and no hypothesis that needs one has been tested [C3].

An AI coding agent works as a loop of model calls: it reads the repository, writes a change, runs the tests, reads the failures and calls the model again. Each call generates text, token by token, on graphics processors in a data centre. Measured on eight models and real software issues, agentic coding used about 1,000 times the tokens of code chat and code reasoning, runs of the same task differed by up to 30 times, and higher token use "does not translate into higher accuracy" [C4]. At list prices one agentic query with a 100,000-token context and 10,000 output tokens costs about $2.50, or about $10,000 a year per developer at three queries an hour, seven hours a day, 200 days a year; that is an illustration, not a measurement [C5]. The International Energy Agency puts reasoning and agentic queries at "hundreds or thousands of times more energy per query than simple text generation" [C6].

Every task. A tool that generates each change pays for generation again on the next task, even when the same change was made before: what the model produced on the first task does not run without the model on the ten-thousandth [C7].

Every retry. Generated code is not repeatable, so a result is bought by sampling again. Asked the same coding question five times at temperature 0, ChatGPT gave answers that differed on every test for 18% to 44% of the problems, depending on the dataset [C8]. Codex solved 28.8% of a set of programming problems with one sample and 70.2% with 100 [C9].

Every language. The same logic shipped in a second language is generated, reviewed and tested a second time, because nothing ties the two versions to one checked source.

Data centres used about 415 TWh of electricity in 2024, about 1.5% of the world's, and the IEA's Base Case projects about 945 TWh in 2030 [C10]. Capital spending by the largest technology companies exceeded $400 billion in 2025 and is expected to rise another 75% in 2026 [C6]. One laboratory's infrastructure project was announced at $500 billion over four years [C11], and Sequoia Capital framed the revenue such spending has to earn back as "AI's $600B question" [C12].

The price of a fixed level of model performance is falling fast, about 13 times a year since 2023 by one measured series [C13], but tokens per task are rising: agentic runs use about 1,000 times the tokens of chat [C4], and the energy per query falls while the tokens per task rise faster [C7]. The RCE project reads these sources as one finding: on the current path every new task, retry and language buys more generation, on more of the same hardware, with more power, and the capital and the electricity grow with use rather than being paid down. That is a reading of the cited figures, not a forecast.

Write the cost of a task as model calls per task times the price of a call, p = n · q [C7]. Better models and cheaper tokens lower q. They leave n where it is: each task, each retry and each language still calls the model. n falls only if work that was checked once is used again instead of being generated again, and that needs a representation in which "the same program" can be decided and a checked result stays checked. The work to reuse exists: about 70% of the code on GitHub consists of clones of files written earlier [C14].

• One checked Form. A program is admitted once by the checker; from then on its behaviour is the fold of δ over its log, which replays bit for bit [C1].
• One Form, many languages. The emitters print the Form as Rust, Python, JavaScript and Scala today, and each emitted program must reproduce the Form's trace; no target is written by hand [C1]. Further targets are proposed in the specification, not built.
• Verified work reused by identity and by behaviour. rce hash gives a program and any renaming of it one hash (theorem T7), and rce equiv decides whether two programs behave the same on the events it explores, printing the shortest event sequence that tells them apart when they do not [C1, C2].

In the design of the engine, a result that passes the checks is stored and closes the next task of the same shape with no model call. That engine is not public code yet [C1].

Joules to completion. A task's completeness predicate C(z), meaning its tests, a proof or an agreement trace, is a constraint: a result meets it or does not. Among results that meet it, approaches are ranked by the energy spent to reach completion, J*, in joules [C1]. Tokens, seats and calls are not the unit, because a reused result spends none of them, while every approach on every machine spends joules.

Public code, at public main 8ce91cea [C2]:

• the specification, draft 0.9, one text at one commit, readable as a notebook at /rce/spec/;
• the reference checker rce 0.1.0, with commands to check, run, test, trace, emit, format, measure the dimension of a program (rce dim), compare two programs (rce equiv, rce change), hash definitions, run a program on a host runtime and replay its log (rce host run, rce host serve, rce host replay), and an in-process database whose store is the log; the same checker runs in a browser at openie-dev.github.io/rce;
• the emitters for Rust, Python, JavaScript and Scala, and the Lean proofs at the levels stated above [C1];
• pinned reference implementations and program corpora for a future lift: 99 programs for Go 1.24, 92 for Python 3.13 and 99 for JavaScript on Node.js 22, each with the recorded output of its run [C2].

• The engine: gears that try lookup, then rules, then synthesis, then a model, last; one gate of replay, a shadow run, a schema check and a proof certificate; promotion of what passes; and receipts with an energy estimate for every decision. The RCE paper describes it as a design [C1].
• Lift, bringing programs written in other languages into Forms. A first lifter covers a defined subset of Python, measured below under question 8; for other languages one probe lifts one Go pattern [C2].
• The RCE-JEPA proposer and its decision head [C3].
• A calibrated energy model per target, so that the cheapest correct target can be chosen; today's estimate cannot tell targets apart [C1].
• The input contract at entry. At 8ce91cea, rce run still drops a payload field that the event does not declare and applies the event; the RCE paper lists the contract as work to finish [C1].
• Idiomatic projections, emitted code that reads as a person in each language community would write it [C1].

Each run below was registered, with its hypotheses and thresholds, before it ran; the rows are public [C15].

• Form space (H1). Over 185 programs, the median ratio of the description length of the emitted Python to that of the Form is 9.34 (interquartile range 8.45 to 10.81), above the threshold of 5; under gzip compression the ratio is 3.57 [C3].
• Adversarial Forms (H7, fuzzed arm). 1,275 mutants that the checker admitted were checked against five stated invariants with 0 violations; the arm with model-written Forms does not exist yet [C3].
• Determinism (H8). 10,500 seeded event streams, traced and hashed on six targets (x86_64, aarch64, big-endian s390x and wasm32, on Linux, macOS and Windows), with 0 mismatching lines [C3].
• Cost of a check. rce check takes a median of 3.0 ms per program (interquartile range 2.6 to 3.8 ms), about 0.03 J at a stated 10 W, labelled an estimate [C3].
• What a program's own examples catch. Of the mutants that change a program's behaviour, its example lines catch 317 of 392 (0.81) [C3].
• Dimension. Four registered runs of rce dim measured how many bits of a program's state change no output. RCE-F6 was triggered on twelve authored two-region programs (median 0.00 bits) and not on the hand-written examples (median 1.29 bits) [C1].
• A model as proposer. A local model with 1.5 billion parameters made 18 proposals of rewrites, 13 of them distinct; the gate did not admit 15, and the 3 it admitted are one rewrite under three names that repeats a rule the engine already had [C1].

Version 1.23 of the RCE paper withdrew every result that only the non-public engine produced, until each is rebuilt on public code with a sealed registration and one command that reproduces it: among them the run on 10,000 generated Forms, the repair rates on the two smallest rungs of the repair ladder, the model checking of the engine's kernel with its check counts, the lift's agreement on four languages, and the test counts at an engine commit [C1]. Figures from earlier slides or decks that quote those results are not current claims.

• est_j: an analytical estimate, for example processor seconds times a stated 10 W, or operation counts priced by a cost table.
• reported_j: a reading of an operating-system or on-chip counter, such as RAPL.
• measured_j: a wall or shunt meter on a named supply, logged with the run, with the idle draw subtracted.

The three are reported in separate columns and never added together, and a cost with no estimate is reported as unpriced, never as zero [C1]. No measured_j exists for RCE: the field is empty in every result, and every energy figure about RCE on this page is est_j [C1].

No measurement compares the two on the same machine and the same tasks. Published figures for generation: LLaMA 65B used about 3 to 4 J per output token, counting graphics-processor energy only [C16], and one median text prompt to a production assistant was measured by its operator at 0.24 Wh, or 864 J [C17]. The 0.03 J estimate for an RCE check is an estimate for a different task, deciding whether a program is in Form, not writing one. The observation that would settle the question is RCE-F3: under a wall meter, gross joules per solved task of the RCE solver against those of the cheapest model baseline on the tasks both solve [C1]. It has not been run.

Current answer. Correct about the hash. rce hash and the log hashes are name-free (theorem T7), so a program and its renaming share a hash, and two programs that reach the same behaviour by different steps do not. No tool can decide in general whether two programs behave the same, which is Rice's theorem [C18], and RCE does not claim to. What it adds is a check for a given pair: rce equiv compares the behaviour of two programs on the events it explores (theorem T58, bisimulation) and prints a distinguishing sequence when they differ, within its exploration bound. Equality at a hash implies equal behaviour; a different hash implies nothing [C1]. Searching a store of programs for one with equal behaviour is part of the engine, which is not built.

Falsifier. RCE-F1: frozen lookup, rules and synthesis resolve under 10% of a held-out set of tasks with no model call [C1]. H10 asks whether canonical Forms halve the examples a proposer needs [C3].

Measurement. Registered and run.

Measured (behaviour index). rce fingerprint now hashes a program's name-free outputs over every event sequence up to a stated length, so that two programs rce equiv judges equal always share it. Over 1,079 program texts, 308 could be fingerprinted; the other 771 are mostly commands with no state to explore. Among 86 pairs that behave the same but differ in shape, the name-free hash matched 0 and the fingerprint matched all 86, and all 187 pairs that rce equiv judges equal shared a fingerprint. At depth 4 and above, 2.0% of the pairs sharing a fingerprint were reported different, none with a distinguishing sequence rce equiv could find. The result supports reuse by behaviour for bounded programs, with equality only up to the explored depth [C19, C20].

Current answer. Correct for explicit exploration: 2⁴⁰ is about 1.1 × 10¹² states. rce dim and rce equiv explore states breadth-first up to a fuel bound, about 100,000 states in 10 to 40 seconds, and report a lower bound when the bound is reached [C1]. The RCE paper says it plainly: finite state makes every question about behaviour decidable and none of them tractable. The symbolic quotient, which would treat each guard as one predicate instead of enumerating its values, is not implemented, and the minimal-machine theorem (theorem T60) is stated, not proved [C1].

Falsifier. No registered falsifier bounds the cost of exploration; RCE-F6 concerns redundant state, not scale. The measurement registered for this critique is the first to put a number on it.

Measurement. Registered and run.

Measured (bounded programs). A checkout with 5 to 80 independent options in one record-typed state: the Form grows linearly, from 12,326 to 113,170 bytes (R² = 0.99996), and rce check takes 5 to 24 ms. The critique holds for exploration: rce dim explores 64 states at 5 options and 4,096 at 10, and reaches its 100,000-state bound at 20 [C19].

Current answer. That is the design. Every step finishes within an explicit bound on evaluation steps (theorem T2); a loop carries a limit, and a with budget block traps with budget when its count runs out [C1]. Non-termination inside a step becomes a recorded trap instead of a hang. What runs indefinitely is the sequence of events, not a step: an event loop or a scheduler is a Form that takes one bounded step per event while the host runtime runs the loop (rce host serve) [C2]. A parser of arbitrarily nested input and a SAT solver have no bound known in advance; in RCE they run under a declared budget and report a trap when it is spent, which is a defined outcome but not an answer. The RCE paper states the consequence for lift: because every Form finishes, a lift from a Turing-complete language reaches only its terminating fragment, and membership in that fragment is undecidable [C1].

Falsifier. H6: any of the reference applications needs an escape hatch outside the Form; RJ-F1: lift coverage stops below 80% on any of five target languages [C3].

Measurement. Registered and run.

Measured (bounded programs). A parser for a subset of JSON with no written bound, no step cap and recursion only on the structure it has parsed returns the right value at every depth from 1 to 4,000 and on every malformed input; the recursive-descent version requires change under W-REC-1. A service of 100,000 events run by the host kept per-block median latency between 3.997 and 4.005 ms, and all 17,766 events that did not apply kept the state, with replay validating all 235,536 log entries. The critique holds for recursion over integers or positions and for backtracking search: a solver for Boolean satisfiability (SAT) by the Davis–Putnam–Logemann–Loveland procedure needs a literal bound 64. Two defects were found: rce test of a deep structural recursion stops with a native stack overflow from depth 807, where the specification promises a defined trap, and moving a value copies it, so the parser's time grows as about depth to the power 2.4 [C19].

Current answer. The premise is right: the checker's verdict is discrete, and one character can change it. RCE-JEPA does not assume smoothness; it states it as a hypothesis to be tested. H11 holds if the energy score rises with edit distance from an admitted Form in at least 80% of test families, and RJ-F4 defeats energy-guided planning in Form space if H11 fails and the search does not reach admitted Forms within its beam budget [C3]. Either way the checker remains the only judge. No proposer exists, so neither has been tested on a model.

Falsifier. H11 and RJ-F4 [C3].

Measurement. Registered and run.

Measured (edit landscape). Over 56 programs, 6 chains of 5 typed edits each, with an energy defined before the run as the number of distinct rules broken plus the share of probe traces that differ: 96.1% of single edits to an admitted program require change, and mean energy rises with edit distance (0, 2.82, 3.75, 4.35, 4.74, 5.13). But only 43 of 56 programs (76.8%) rise steadily, below the 80% H11 needs, so H11 fails, narrowly; and a greedy descent from three edits away returns to an admitted program of the same behaviour 2.1% of the time against a registered threshold of 50%, so RJ-F4 is observed. The energy is defined by hand, not a model's, so the result is about this score [C19].

Current answer. Correct. The checker shows that a Form is well formed and meets its stated examples and checks; it does not show that the Form is what was meant, and a table of the example answers meets the examples. The RCE-JEPA paper lists this risk as specification gaming, labelled and not solved [C3]. One measurement exists: of the mutants that change a program's behaviour, the program's own example lines catch 317 of 392 (0.81, Wilson 95% interval 0.77 to 0.85), and almost all that they miss are a constant moved by one that no example exercises [C3].

Falsifier. RJ-F2: writing the intent for the reference applications costs more person-hours than writing their Forms by hand [C3]; RCE-F2: byte-identical or equivalent patches are under half of the resolved held-out tasks [C1].

Measurement. Registered and run.

Measured (table control). Each program with examples was rebuilt as its lookup-table control, equal to the program only on its example event lists. The checker admits all 56 controls, the stated obligations tell none of them from the program, and all 56 differ from it away from the examples. rce check now prints a recommended change, rule W-INT-2, when a module's example lines are its only obligations, without changing the verdict [C19, C20].

Current answer. Correct that a pure step does not prevent faults in the network or the clock. What RCE changes is that the boundary is recorded. Every input, tick and external answer is an entry in the log, so replay reproduces exactly the order the host observed (theorems T3 and T32), and rce host replay re-derives every state hash with every adapter disconnected [C1, C2]. Time inside a program is the logical clock only, so skew is an input the log records, not a hidden variable [C1]. Duplicates and drops remain the host's to handle: the engine's design requires that a full mailbox hold its messages and log the back-pressure instead of dropping them, and rules that are monotone need no coordination between replicas, by the CALM result [C1]. Neither has been measured.

Falsifier. None is registered. H8 covers the replay of recorded streams, not faults in the world [C3].

Measurement. Registered and run.

Measured (host faults). A seeded harness drove 9 programs on the real host through 72,000 runs with dropped, duplicated, reordered and lost messages, kills mid-batch and clock steps. The host contract held in every run: replay reproduced the live state exactly, every entry was a step or a kept step, no restart reused an id, and inputs with a source and sequence number were applied exactly once. The programs did not: a duplicated withdrawal was applied twice in 912 of 1,000 runs, a retried delete was answered 404 in 330, and a rate limiter exceeded its true-time limit after a forward clock step in 490. RCE makes these faults replayable and detectable; it does not prevent them, and exactly-once delivery is reachable today only through the embedding interface [C19, C20].

Current answer. Part of the cost is real by design. Floating-point numbers are IEEE 754 binary64, rounded once per operator on every target, so a fused multiply-add, which rounds once for two operations, cannot be used where it would change a bit; and every step's state is hashed with SHA-256 into the log [C1]. The figure of 10 to 100 times slower is a claim, not a measurement: no RCE paper reports a speed comparison with conventional code. What is measured is the determinism itself: 10,500 event streams on six targets with 0 mismatches [C3].

Falsifier. H4: energy per admitted program is not lower than the baseline's [C3]; RCE-F3: under a wall meter, joules per solved task exceed those of the cheapest model baseline [C1].

Measurement. Registered and run.

Measured (determinism cost). Eleven programs, 1,000 events each, processor time: the hash-chained log costs a median 2.55 times the bare step in the checker and 5.35 times in emitted Rust; the rule against fused multiply-add costs about nothing (0.65 to 1.06 times). The claim of 10 to 100 times does not hold for the log as stated. Two costs are larger: emitted Rust is a median 388 times slower than hand-written Rust, because of its value representation rather than determinism, and hashing the full state every step costs a median 1,268 times a native step, so for fast native code the critique understates that cost. Energy for these runs is est_j only [C19].

Current answer. Correct for most real code. Until 29 October 2026 no lifter existed in public code; at 8ce91cea one probe lifts one Go pattern, a struct with one method per event, into a Form, and what is in place is the other side of the comparison: pinned implementations of Go, Python and JavaScript with 99, 92 and 99 programs and the recorded output of each run [C2]. The RCE paper bounds what any lift can do: it reaches only the terminating fragment of a language, and how closures, control states and evaluation order are represented are free choices, so a lifted Form is not canonical [C1]. Dynamic dispatch, exceptions and unbounded retry loops each need a construction that has not been written.

Falsifier. RJ-F1: lift coverage stops below 80% on any of five target languages [C3]; and the lift gate of the RCE programme: coverage under 10% on any of the first four languages after the second registered run [C1].

Measurement. Registered and run.

Measured (lift, Python). The first lifter, for a defined subset of Python 3.13, now exists. On the 92 pinned corpus programs it lifts 6 that reproduce the recorded run, gives 0 wrong results, and reports every other case as requiring change under a named rule (most often unsupported calls, imports, types and exceptions); on the 15 functions of heapq.py it lifts none. Coverage is far below the 80% of RJ-F1; RJ-F1 is judged at a plateau, after the list of constructs is exhausted, which it is not [C19, C20].

Current answer. Correct today. Emitted code is a dynamic-value runtime per target, four hand-written runtimes of about 2,000 lines each, printed so that it reproduces the trace, not so that it reads like code a person in that language community would write [C1]. The RCE paper's position, that a projection should render layout and idiom for each community from a structured record of the names and intent, is stated and not built [C1]. A step is pure, so an ecosystem library is not called from inside one: effects go through host adapters and declared foreign calls, whose answers are logged so that replay still holds (theorem T32) [C1].

Falsifier. The encapsulation criterion of the RCE paper: a language on which the Form is strictly worse on any of five coordinates (joules, redundancy, decidability, the round trip, and the cost to reach a program that passes) after two registered runs is not encapsulated [C1]. No run exists.

Measurement. Registered and run.

Measured (projections). At 8ce91cea no emitted program could be embedded in another program. After a change of 27 lines to the emitters, eight services embed them, in Python (asyncio, FastAPI, numpy), Rust (tokio) and JavaScript (node:http, React and a host with no Node.js runtime), and each reproduces the trace of rce run byte for byte on 11 of 11 event streams. The critique holds on two points: emitted code is 4.2 to 6.9 times the lines of a hand-written version, and in Rust converting at the boundary takes more than half of each call [C19, C20].

Current answer. Specification is where the cost moves, and it can be large. In seL4, a verified operating-system kernel, the abstract specification took about 4 person-months and the proof about 20 person-years, against 2.2 person-years to build the kernel [C21]. In a 2026 study of verified synthesis driven by a language model, the dominant failures "were not failures of bounded verification, but failures of specification coverage" [C22]. RCE does not remove this cost; RJ-F2 makes it measurable [C3].

On demand: cheaper tasks can raise total use. A venture essay expects it ("we believe Jevon's Paradox in this case holds") [C5], and the one published elasticity, across tasks in one provider's sample, is about −0.29, a cross-section rather than a price change over time [C23]. RCE's claim is about joules per completed task, not total joules: reuse lowers the cost of a repeated task, and whether total energy then rises with new tasks is a question about demand that no RCE result answers [C7].

Falsifier. RJ-F2 for the cost of specification [C3]; for demand, none in the RCE papers.

Measurement. Registered and run, for size and sufficiency; RJ-F2 itself, a timed study of authoring in person-hours, was not run.

Measured (specification cost). Over the 60 programs of the corpus that state an intent or example lines, all written by the RCE project, the obligations (example, check and contract lines) have a median size of 0.37 of the program body in bytes (interquartile range 0.26 to 0.51), and only 3 exceed it. They are also partial: of 461 single changes to a body that alter its behaviour, judged on the example streams, 64 random streams and rce equiv, the obligations catch 327 (0.709, Wilson 95% interval 0.666 to 0.749); judged on the example streams alone, as in the earlier figure of 0.81, they would appear to catch 0.864. What they miss is mostly a literal or a comparison at a boundary no example exercises. So writing the obligations costs less than writing the code here, and obligations of that size do not pin down behaviour; making them complete would make them larger, which supports the critique in part. No measurement in the RCE papers yet settles the question of demand [C19].