Etch is an experimental programming language whose compiler rejects any program it cannot prove safe to run. Before a program starts, the compiler checks integer ranges, array bounds, termination, aliasing between names, and which parameters each function may write.
The compiler is written in Etch and compiles itself. It includes an interpreter and an arm64 backend that emits machine code directly, without LLVM or C.
7f9fff9f · 2533 commits · updated 2026-10-02 · source not yet public — repo links go live with the release
fn g(y: int(0..9)) -> int { return y; }
fn f(x: int(0..20)) -> int {
if x == 10 {
return 0;
} else {
return g(x);
}
}
fn main() {
println(f(5));
}error: call to g: argument `y` not proven ⊆ [0, 9] (got [0, 20])
In the else branch x can still be anything in [0, 20] except 10, which is outside g's parameter range, so the compiler rejects the program even though main only passes 5.
Each example below is a file in tests/cases/, shown with the current compiler's output.
An integer type can carry a range. Every call is checked against the parameter's range using what the compiler can prove about the argument. Here b is exactly 12.
fn f(x: int(0..10)) -> int { return x; }
fn main() {
let a = 6;
let b = a + 6;
println(f(b));
}error: call to f: argument `x` not proven ⊆ [0, 10] (got [12, 12])
Integers are limited to ±(253−1), a range every backend and host computes exactly. Arithmetic that provably leaves it is a compile error.
fn main() {
let a = 1000000;
let b = a * a * a * a;
println(b);
}error[E_OVERFLOW] (refinement) fn main, stmt 1: arithmetic provably escapes the int domain [fix-class: evidence]
Every loop and recursive call needs a measure that decreases, either one the compiler finds or one written with decreases. Functions cannot be marked partial. In this loop i never changes.
fn f(n: int) -> int {
let i = 0;
let acc = 0;
while true {
acc = acc + 1;
if i >= n { break; }
}
return acc;
}error[E_TERMINATION_EVIDENCE] (termination) fn f, stmt 2: loop/recursion without provable ranked measure [fix-class: evidence] [subject: `while true`] [retiring-evidence: a `decreases <var>` measure, or the counting form `while i < n { …; i = i + 1 }` with `n` loop-invariant]
Every index must be proven in bounds. The guard proves a[2], and the pop through a ends that proof: a write to a name drops what was known about its length.
fn main() {
let a: []int = [1, 2, 3];
if 2 < a.length() {
a.pop();
println(a[2]);
}
}error[E_INDEX_UNPROVEN] (refinement) fn main, stmt 1: index not proven in bounds — guard it, iterate 0..xs.length(), or use checked_get [fix-class: evidence]
Binding an array to a second name does not copy it; the second name borrows it. Writing through the original while the borrow is still used is rejected, so a fact proven through the borrow cannot be changed behind its back. A copy is made only where the program calls clone.
fn main() {
let a: []int = [1, 2, 3];
let b: []int = a;
a.push(4);
println(b.length());
}error[E_BORROW_OWNER_WRITE] tests/cases/borrow_owner_write_push_reject.etch:main:0.1: `a` is written by `.push()` while its view `b` is live (RFC 002 §7.1); fix-class: clone at the view (`.clone()` on the value `b` names) or move the write past the view's last use
Parameters are read-only. A function that writes one must say so in its signature with effects { write(x) }, so callers can see every argument a call may modify.
fn f(x: int) -> int { x = x + 1; return x; }error[E_PARAM_WRITE] (structure) fn f, stmt 0: parameter `x` is written but the declaration does not authorize it — add `effects { write(x) }` to the signature, or derive a local (`let q = x;`) if only a local value is meant (RFC-002 §7.2) [fix-class: evidence]
derived defines a value computed from other values; its dependencies are the names its body reads. A write marks dependents stale, and a derived value is recomputed when it is next read, only if one of its inputs changed value.
fn main() {
let a = 1;
derived b { a + 10 }
derived c { a + 100 }
derived d { b + c }
println(d);
a = 5;
println(d);
}112 120
An effect that writes a value it depends on forms a cycle. A cycle is admitted only with a proof that it converges. The compiler accepts one form of proof: the effect writes the value once, as min(g, K) or max(g, K), where K does not depend on the value and g is non-decreasing in it and at least the value (at most, for max). Each write then moves the value toward K without passing it, so it settles in finitely many steps. Here a = 5 makes da 6, so the effect writes 3; da becomes 4, the effect writes 3 again, and the unchanged write ends the cascade.
fn main() {
let a = 1;
derived da { a + 1 }
effect { a = if (da < 3) { da } else { 3 }; }
a = 5;
println(a);
}3
The same proof covers a ring of effects, where each effect reads one value of the cycle and writes the next. A write then goes once round the ring before it comes back, so the ring behaves like one effect writing the composition of its writes. Every write in the ring must be a min of this form, or every one a max. Here a = 1 drives b to 2, a to 3, b to 4, a to 5 and b to min(6, 5) = 5; the next write to a is also 5, unchanged, and that ends the cascade.
fn main() {
let a = 0;
let b = 0;
derived da { a + 1 }
derived db { b + 1 }
effect { b = min(da, 5); }
effect { a = min(db, 5); }
a = 1;
println(a);
println(b);
}5 5
Without a bound the writes never stop, and the cycle is rejected. So is a cycle whose effects branch, such as an effect reading two values of the cycle, and a derived body can only read names declared before it, so a cycle between derived values cannot be written.
fn main() {
let a = 1;
derived da { a + 1 }
effect { a = da; }
a = 5;
}error[E_CYCLE_UNPROVEN] (convergence) fn main, stmt 2: effect writes `a`, closing a cycle through its own trigger set without N6 monotone_bounded evidence (the value written to `a` is not a min or max with a bound; the discharged shape is a single `a = min(g, K)` or `max(g, K)` with K independent of `a` and g non-decreasing in `a`, at least `a` under min and at most under max) [fix-class: evidence]
Ranges are not inferred from call sites. g declares nothing about z, so the compiler cannot decide whether the call to f is in range. The compiler implements only the strict profile, in which an undecided check is an error. The specification also defines a checked profile, in which it becomes a runtime check that is recorded as outstanding proof work (RFC 007).
fn f(x: int(0..10)) -> int { return x; }
fn g(z: int) -> int { return f(z); }
fn main() {
println(g(3));
}error: call to f: argument `x` not proven ⊆ [0, 10] (got unknown)
The backend has no optimization passes of the LLVM kind: no alias analysis, loop-invariant code motion or bounds-check elimination. The facts those passes would recover are established while the program is checked, and the backend uses them directly. In the matrix multiply below, the shaped type [n][n]int fixes every row's length at n, so no index in the inner loop needs a bounds check.
fn mul(a: [n][n]int, b: [n][n]int, n: int) -> int {
let acc = 0;
for i in 0..n {
let ra = a[i];
for j in 0..n {
let s = 0;
for k in 0..n { s = s + ra[k] * b[k][j]; }
acc = (acc * 31 + s) % 1000000007;
}
}
return acc;
}tests/perf-clang-parity.sh compares each workload with the same algorithm written in C and compiled with clang -O2. The outputs must be identical, and Etch's time must stay within a fixed multiple of clang's. Latest figures, as Etch time divided by clang time:
| Workload | What it does | Etch / clang |
|---|---|---|
| getter | reads a derived value 200,000 times; its input changes 200 times | 0.019 |
| str_scan | sums the bytes of a string | 0.19 |
| array_sort | insertion sort | 1.1 |
| str_build | concatenation, toString, split | 1.3 |
| closure_calls | a fold calling a closure | 1.5 |
| int_loop | arithmetic and modulo in a loop | 1.6 |
| str_parse | a state machine over bytes | 1.7 |
| map_ops | string-keyed map inserts and lookups | 1.8 |
| rec_calls | recursive fib | 1.9 |
| struct_step | updates fields in an array of structs | 1.9 |
| match_vm | a stack machine matching on an enum | 1.9 |
| write_heavy | writes a derived value's input 20,000 times, reads it 20 times | 2.0 |
| matmul | the matrix multiply above | 2.6 |
Both versions are compiled for arm64 and run under qemu-user on x86_64 Linux; minimum of 5 runs, 2026-09-27. Emulation changes some ratios compared with native hardware. The C version of getter recomputes the value on every read, which is where the difference comes from. Details are in RFC 025 §6.1.
Etch is a research project. The compiler implements part of the specification.
checked profile and proof debt (RFC 001, RFC 007).min/max form above is implemented, for one effect or a ring of effects.error[E_…] form, and part of the corpus still expects the older wording.The compiler is built by a checked-in compiler binary, bootstrap/etch-seed, which runs directly on arm64 macOS. On Linux, tools/macho-run runs it and the programs it builds, using qemu-user on x86_64. Run the commands from the repository root.
# Linux only
sudo apt-get install qemu-user-static gcc-aarch64-linux-gnu # x86_64 hosts
tools/macho-run/install
export PATH="$PWD/tools/macho-run/bin:$PATH"
# generated sources (node 22.6 or later)
git submodule update --init
export NODE_OPTIONS=--experimental-strip-types
node grammar/gen.ts
node tools/gen-builtin-tables.ts
# build the compiler (it prints its usage line at the end)
ETCH_NATIVE_BIN=$PWD/etch bootstrap/etch-seed src/main.etch --native
./etch file.etch # check, then interpret
./etch file.etch --native # check, compile and run
bash tests/run.sh # all tests, about 10 minutesBuilding an unchanged tree reproduces the seed byte for byte. HANDOVER.md describes how to update the seed and how to check a performance change.
The language is defined by the RFCs in docs/. They describe the intended language, including the parts listed above as not yet implemented. RFC 001 states the invariants the others build on.
12 RFCs.