The compiler proves what it tells you.
Mettle is a systems language. It compiles to native x86-64 through its own backend, its own linker and its own debugger. No LLVM. No virtual machine. No external assembler.
That is the smaller claim. The larger one is a rule the compiler keeps everywhere: it never asserts what it has not proven.
When your program is wrong
── main.mettle:6:20 ────────────────────────────────────────────────
error[E0003]: Function 'add' expects 2 arguments, got 3
────┬───────────────────────────────────────────────────────────────
5 │ fn main() -> int64 {
6 │ var r: int64 = add(1, 2, 3);
· ^^^ expected 2 arguments, got 3
7 │ return r;
────┼───────────────────────────────────────────────────────────────
│ note function 'add' defined here
1 │ fn add(a: int64, b: int64) -> int64 {
· ^^^
help: pass 2 arguments, or change 'add' to take 3
The caret marks the span, not the line. The note points at the declaration
the call disagrees with. Every code has
a page here and the same words in your terminal
under mettle explain E0003, because both read one table.
When your program is right
── optimization report: main.mettle ────────────────────────────────
sum (loop @ line 7): vectorized → vpaddd, 8-wide int32 sum (AVX2)
main (loop @ line 18): NOT vectorized [store-only-fill]
18 │ for i in 0..8 {
19 │ data[i] = (int32)i + 1;
└─ reason: the loop fills the stack array `data`, whose address is
retaken on every iteration; the fill kernel indexes off one
invariant base pointer, and a fresh base each iteration is not one
└─ fix: bind the array to a pointer once before the loop
(`var p: int32* = &data[0];`) and write `p[i]` in the body
└─ verified: simulated that fix and re-ran the optimizer: this loop
then vectorizes → 8-wide int32 element-wise map, bit-exact
Read the last line again. The compiler did not guess that the fix would work. It copied the function, applied the fix, ran the optimizer again and looked at what came out. Advice that fails that test never reaches you.
Four rules
-
It never asserts what it has not proven.
The borrow checker points only at mistakes it can prove, so it never rejects a program that works.
--explainruns its own advice before printing it.@simd!,@inline!and@noallocstop the build rather than quietly do less than you asked.--verifyruns every pass on every function, before and after, and compares. Where it cannot check something it says so. -
One machine, many products.
The IR interpreter runs
mettle test,mettle trace,--pgo,--verify, the leak checker and the gate on the learned optimizer. Your tests and the optimizer are held to one set of semantics, so the two cannot drift apart. -
Pay for what you use, and prove you did not pay.
Runtime helpers link only when your object refers to them, and
objdump -twill show you which ones did.@noallocproves a call graph allocates nothing rather than asking you to believe it. A cost you cannot check you avoided is a cost you still carry. -
Declare what you mean. Let the compiler work out what is safe.
Every
varcarries its type; nothing is inferred. The compiler works out lifetimes, aliasing, and whether a loop can vectorize. Types are what you meant. The rest is a consequence.
What it costs
On data-parallel kernels the vectorizer beats gcc 13.3 -O3,
by up to 5.9x on float sums and scans. On whole applications it loses. Across
eight programs it lost all eight to clang -O3, by 1.33x on average
and 1.9x at worst. Serial and call-heavy code is where it gives the time
back.
| runtime, 8 applications | 1.33x slower |
| compile time | 6.5x faster |
| binary size | 9x smaller |
Measured 20 August 2026 on an i7-12700K. The harness, the sources and the raw numbers are in docs/benchmarks, so you can run them yourself and disagree.
Try it
curl -fsSL https://raw.githubusercontent.com/suidvandiewereld/Mettle/main/install.sh | sh
Then save this as hello.mettle:
import "std/io";
fn main() -> int32 {
println("Hello from Mettle.");
return 0;
}
mettle --build --release hello.mettle
Windows and Linux, x86-64. The compiler builds and links the binary itself.
Read on
- Inside the compiler, one stage at a time
- Reading a diagnostic
- Reading the report
- Every code the compiler can print
- The ideology, which is the decision procedure the four rules come from