■Rust
You write references (&, &mut) and lifetimes. The borrow checker proves no two names alias and mutate at once, so memory is freed deterministically. You pay with the annotations, and you get zero-copy where the borrow allows.
Reactivity is the language, not a library. derived recomputes when its inputs change, and the compiler proves that recomputing only what changed equals recomputing everything. No subscription bookkeeping, no dirty marking, no glitches. Reactive and memory safety are the same problem: tracking who reads and writes what. Solve reactivity, and the analysis a borrow checker would do is already done — for free. The same move then generalizes to safety, memory, determinism, and performance.
etch hello.etch // compiles to a native binary
./hello // prints helloA program, in hello.etch:
fn main() {
println("hello");
}etch emits machine code directly — no clang, no LLVM, no outside optimizer. The compiler is self-hosted. The only outside parts are the system linker and the debug format, listed in note 1 of section 伍.
Etch's core is that derived and effect are language primitives, not a runtime library. derived declares a value that recomputes when its inputs change; effect runs after each change. The compiler knows the dependency graph, so incremental updates are proven equal to full recomputation (incremental ≡ from-scratch).
let count: int = 0;
derived doubled { count * 2 }
effect { println(toString(doubled)); } // prints 0 now
fn main() {
count = 1; // prints 2
count = 2; // prints 4
}This toy leaves out the effect rows: main writing the global count, and the effect reading doubled, are carried by inferred rows in the function signatures. A full listing would print those rows beside the signatures. (Here effect is the reactive block, not the effect row in a function's type.)
This works because Etch commits the work a reactive runtime used to do — subscription bookkeeping, dirty marking, topological sorting — into the compiler as spec. You don't manage subscriptions, write dependency arrays, or worry about glitches. That's the name: the reactive behavior is etched into the machine code at compile time — there is no runtime to erase it.
Even cycles are handled: a cycle in the reactive graph is admitted only if the compiler can prove it converges. Concretely, a derived that tracks a running maximum — best reads its own previous value and the newest score, joined by max — is a cycle, but max is monotone and bounded (the value only rises, and scores are finite), so the compiler proves it reaches a fixed point instead of looping. A cycle with no such proof is rejected.
The same move applies everywhere. Value semantics — owned values copy; &ref is the scoped by-reference escape. Effect rows — what a function reads or writes is in its type. Prove-or-reject — safety and termination are proven up front, or bounded by a named limit. Regions — no garbage collector. Bit-identical determinism — the same result on every machine. Integers are 64-bit; a range like int(0..9) is itself a type, so bounds travel with the value.
If it compiles, you can rely on:
match.Option/Result you must handle.f64 package is specified separately.One rule runs through the whole language: a cost isn't forbidden — it's named and listed. The tax bill (section 柒) is where those costs get itemized.
budget (like fn main budget 256MiB)fueled limit (running out becomes a value, not a crash)The checker isn't perfect: some programs that would stop still get rejected (Collatz is the usual example). Restructure the loop or add a fueled bound.
fn clamp(x: int(0..100)) -> int { return x; }
fn main() {
println(clamp(50)); // 50
}This program compiles and runs. The interpreter is a second, independent implementation of the language, kept to check that the compiled version agrees with it — both give the same result here (prints 50). Grounded in RFC 001.
Pass an argument it can't prove, and it rejects the program, naming the missing proof:
fn clip(x: int(0..10)) -> int { return x; }
fn main() {
clip(11);
}error: call to clip: argument `x` not proven ⊆ [0, 10] (got [11, 11])No garbage collector isn't the hard part — Rust already has that. The hard part is no GC without the borrow checker's lifetime annotations. Etch gets both.
You write references (&, &mut) and lifetimes. The borrow checker proves no two names alias and mutate at once, so memory is freed deterministically. You pay with the annotations, and you get zero-copy where the borrow allows.
Owned values copy (copy-on-write); &ref is the scoped by-reference escape, with no lifetime annotations to write. The read/write sets the reactive graph already needs — effect rows — are the same information the borrow checker otherwise enforces through annotations; Etch has it because reactivity required it anyway. Regions reclaim memory: bump allocation, bulk release at frame exit, O(1), no GC.
Concretely, a function that returns one of two borrowed strings:
Rust — you write the lifetime:
fn longest<'a>(x: &'a str, y: &'a str) -> &'a str {
if x.len() > y.len() { x } else { y }
}Etch — values copy, nothing to annotate:
fn longest(x: string, y: string) -> string {
if x.length() > y.length() { x } else { y }
}The cost just moves. Etch pays implicit copy-on-write copies (named in the build report) and a compile-time proof of region lifetimes and memory bounds; Rust pays explicit borrow and lifetime annotations.
Etch emits machine code directly — there is no LLVM, no clang, no external optimizer in the path.
Four reasons:
Every cost is named in the source (P1, P3). An outside optimizer would rewrite the code afterward, so the named costs would describe a program that no longer exists.
The object-level proofs depend on a fixed source-to-output correspondence. Optimizer passes break that correspondence, turning the proof from hand-auditable into "prove an entire optimizing compiler".
A program that needs an optimizer has already lost information. Etch's fixes are in the language — elaboration, the instruction vocabulary, the proofs — not in a backend rewrite.
On compiler-class workloads, the optimizer's -O1 to -O3 spread measures about zero — it has nothing to add there.
Performance comes from source instead: the instruction vocabulary (one word = one or two machine instructions) and the named costs, covered in section 柒. The only outside parts are the system linker and the debug format, named in note 1 of section 伍.
The chart plots two things: how directly you control the machine, and how much the compiler can check. The exact corner is empty. Etch sits beside it.
Same bug, three outcomes. Reading one past the end of an array: C — undefined behavior; Rust — a runtime panic; Etch — a compile error naming the missing proof.
Memory uses region-based allocation: one forward sweep to take it, one bulk release to give it back — no per-object malloc/free.
When the compiler has already proved an index is safe, it emits no bounds check and no defensive copy. The proof comes from the language, not from a smart optimizer.
Who reads and writes what is part of a function's type. Because the compiler knows that, it can run independent work on separate cores and still get the same result no matter how many cores are used — that is what "deterministic parallelism" means here. Hand-written parallelism in C or Rust doesn't give you that guarantee.
Performance depends on the workload. Code that allocates a lot, walks linked data, runs in parallel, or runs repeatedly benefits. A simple loop over integers does not. No performance claim is made for anything else. See RFC 007.
P1 — no hidden waits. Operations the hardware can't predict — random reads, branches that depend on data, indirect calls, atomic operations, calls into the operating system — must be named in the source. A named operation is a site you can point to in the code: for example, a table lookup written t.get(k) is a random read, and the compiler lists that exact site as a wait. Nothing in this class is added silently by the backend.
P2 — you can name machine instructions. A fixed set of source words, each mapping to one or two machine instructions per target — for example, popcount (count one-bits), fused multiply-add (multiply and add in one step), and charclass (classify a byte). Anything outside the set is emulated, and that emulation is listed in the tax bill.
The tax bill. The same five costs section 貳 names, itemized here, followed by the performance costs Etch keeps visible:
budget).budget (fn main budget 256MiB).fueled limit; running out becomes a value, not a crash.Two examples: type-checked bounds and memoization. Each compiles and runs; the interpreter and the compiled version give the same result.
fn g(y: int(0..9)) -> int { return y; }
fn f(x: int(0..20)) -> int {
if x < 10 { return g(x); } // x < 10 refines x to int(0..9)
return 0;
}
fn main() {
println(f(9)); // 9
println(f(15)); // 0
}memo fn caches a pure function's result.
memo fn double(x: int) -> int { return x * 2; }
fn main() {
println(double(21)); // 42
}UI building blocks work the same on every platform. A small core is built in — just the primitives that make those building blocks uniform across platforms. Everything else, such as widgets and application structure, is written in user code, and user code costs the same as the built-in parts.
UI targets: web DOM (wasm32), macOS / iOS, android, terminal (a text-based interface, TUI).
Every cost is written down, so an AI can reason about performance instead of measuring a black-box optimizer. Judge mode scores a code change (a diff between two versions of the program) against the cost model: it lists which named costs — waits, emulation, allocation, effects — were added or removed, so an agent can see whether the change made things cheaper or more expensive. Error messages, effect lists, and traces are machine-readable; that's the interface an agent uses.
etch.c), and each rebuild matches the previous output byte for byte.The RFC index below is generated by site/gen.etch — run site/gen-rfc.sh to regenerate it from docs/rfc-*.md.
&ref is the scoped by-reference escape (no lifetime annotations to write).fn f(xs: &ref)) refers to the caller's value for the call's duration; mutation through it is observable and drives recomputation.int(0..9) that constrains a value to an interval.f64 package is specified separately.fueled limit that ends it. Indexes stay in bounds and division is never by zero.fn main budget 256MiB; it sizes the region the program runs in, and running out is the one named abort.fueled(1000) (a step count); running out becomes a value, not a crash.etch.c.