A programming language where the compiler proves your code safe before it runs.
clang -O2.Self-hosted compiler · arm64 backend · no LLVM or C
644b9c35 · 3061 commits · updated 2026-10-14 · source not yet public — repo links go live with the release
The compiler rejects programs it cannot prove safe. When it does, it shows you the line and a short error. Full diagnostics and test file paths are available in a collapsible detail.
Argument b = 12 exceeds parameter range int(0..10)
fn f(x: int(0..10)) -> int { return x; }
fn main() {
let a = 6;
let b = a + 6;
println(f(b));
}fn f(x: int(0..10)) -> int { return x; }
fn main() {
let a = 6;
let b = a + 4;
println(f(b));
}argument not proven inside interval
tests/cases/d53_r3a1_call_rej_straight_oob.etch
error[E_REFINED_STORE_UNPROVEN] (refinement) fn main, stmt 2: argument to an int(lo..hi) parameter not proven inside its interval by the index prover — guard the value before the call (an if, an early return, min or max) [fix-class: evidence]Arithmetic escapes ±(253−1)
fn main() {
let a = 1000000;
let b = a * a * a * a;
println(b);
}fn main() {
let a = 1000000;
let b = a * a;
println(b);
}arithmetic provably escapes the int domain
tests/cases/arith_oob_straightline.etch
error[E_OVERFLOW] (refinement) fn main, stmt 1: arithmetic provably escapes the int domain [fix-class: evidence]Loop variable 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;
}fn f(n: int) -> int {
let i = 0;
let acc = 0;
while i < n {
acc = acc + 1;
i = i + 1;
}
return acc;
}
fn main() { println(f(10)); }loop without provable ranked measure
tests/cases/total_reject_break_no_incr.etch
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]Write to a drops the proof that a[2] is in bounds
fn main() {
let a: []int = [1, 2, 3];
if 2 < a.length() {
a.pop();
println(a[2]);
}
}fn main() {
let a: []int = [1, 2, 3];
if 2 < a.length() {
println(a[2]);
a.pop();
}
}index not proven in bounds
tests/cases/bounds_reject_owner_pop.etch
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]Write through a while borrow b is live
fn main() {
let a: []int = [1, 2, 3];
let b: []int = a;
a.push(4);
println(b.length());
}fn main() {
let a: []int = [1, 2, 3];
let b: []int = a.clone();
a.push(4);
println(b.length());
}owner written while view is live
tests/cases/borrow_owner_write_push_reject.etch
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 usechecked_get returns an option that must be exhaustively matched
fn unsafe_get(xs: []int, i: int) -> int {
match checked_get(xs, i) {
.some { v } => { return v; }
}
return 0;
}fn safe_get(xs: []int, i: int) -> int {
match checked_get(xs, i) {
.some { v } => { return v; }
.none => { return 0 - 1; }
}
}
fn main() {
let xs: []int = [10, 20, 30];
println(safe_get(xs, 1));
println(safe_get(xs, 5));
}match does not cover variant(s): none
tests/cases/error_handling_checked_get_reject.etch
error[E_NONEXHAUSTIVE_MATCH] (structure) fn unsafe_get, stmt 0: match does not cover variant(s): none [fix-class: evidence]Etch has no exceptions or panics. Operations that can fail return option or enum types that must be matched exhaustively. checked_div, checked_mod, and checked_get are built-in fallible operations. The Outcome type and checked profile for recoverable errors are specified in RFC 011 but not yet implemented.
Function writes parameter x without declaring effects { write(x) }
fn f(x: int) -> int { x = x + 1; return x; }fn f(x: int) -> int { let y = x + 1; return y; }
fn main() { println(f(1)); }parameter written without authorization
tests/cases/256_param_write_scalar_reject.etch
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 values recompute when dependencies change
fn main() {
let a = 1;
derived b { a + 10 }
derived d { b + a + 100 }
println(d); // 112
a = 5;
println(d); // 120
}Effects that form cycles must converge
fn main() {
let a = 1;
derived da { a + 1 }
effect { a = if (da < 3) { da } else { 3 }; }
a = 5;
println(a); // 3 — converges
}
fn diverge() {
let a = 1;
derived da { a + 1 }
effect { a = da; } // rejected: no bound
a = 5;
}Cycles admit min(g, K) or max(g, K) with K independent of the value
More checks: derived bodies, undecided proofs, reactive read sets — see Specification
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.