From the silicon up: a language that proves itself

Most languages are written for people and then, with effort, made fast for machines. QUANTA is the other way round: a language an AI writes, and a machine proves correct, from the silicon up. It is not a wrapper over LLVM or a DSL that lowers to someone else's runtime. It is a compiler, four backends, and a growing standard library, built so that the proof travels with the code.

This page is the deep, honest account of what is measured today — and, in the same breath, what is still open. That second half is not a disclaimer. It is the point: a claim you can check is worth more than one you can't.

The self-hosting proof: byte-identical, twice

✅Shipped & measured

The headline result is a costly signal a competitor cannot fake on a slide. qc2, the QUANTA compiler, compiles itself — and we verify the output with diverse double-compiling: build the compiler with gcc, build it again with clang, and compare the bytes. The output is byte-identical. 🟢 (We used to print a module count here; it is not stated in any current source document, so we have removed it rather than restate a number we cannot show you.)

Why this matters: identical bytes from two independent toolchains is evidence that no compiler has smuggled anything into the binary — the classic "trusting-trust" attack. The agreement is the proof. It is the same discipline a safety assessor applies to a signalling system: don't trust the tool, verify the artefact.

The front-end now clears an even higher bar. qcc11 — a code generator written in QUANTA — compiles the full qlexer.q and qparser.q (a real five-parameter lexer and a recursive-descent parser with Pratt precedence), and the native output matches the interpreter exactly. QUANTA now lexes and parses QUANTA, in QUANTA. We are roughly one or two language features (use plus closures, both landed) from the complete fixpoint.

Four backends, one gate

✅Shipped & measured

The same source compiles gate-clean to four backends: x86-64, ARM64/NEON (run under QEMU, exact), PTX for the GPU, and portable C. 🟢 Every one is held to the same rule — the native result must equal the interpreter's — so "runs on any chip" is not a marketing line, it is a passing test on four targets.

Two capabilities make this more than a toy compiler:

• Cost-as-type. Accuracy and cost are carried in the type system. A cost-model picks the strategy, which is how the register allocator went from 25.8 to 9.6 cycles per call — 4.2× faster and 3× smaller at once 🟢 — and how a matmul reaches 0.8 TFLOP/s with no BLAS library underneath.
• Cryptography against published vectors — where it holds, and where it did not. SHA-2/3 and BLAKE3 validate against their published vectors, and chacha20_block matches the RFC 7539 KAT exactly. 🟢 The AES and HMAC chapters did not survive the same check and are quarantined in the Ledger: the AES chapter cites a NIST AES-CTR vector its main() never asserts against, a function named hmac_sha256 has "XOR all bytes" for a body, and a "CSPRNG" turned out to be a bare linear congruential generator with no entropy source. These are the tests you cannot bluff — which is exactly why they caught us.

Languages in, languages out

✅Shipped & measured

QUANTA imports and exports, gate-verified in both directions. c2q proves a C function equivalent to its QUANTA translation per-function (sum, dot, count_pos all verified equivalent); py2q and a Rust path do the same coming in. Going out, QUANTA emits portable C plus the three native backends — a four-target Rosetta stone for code.

What is still open

🔬Research

Kept visible, because the tiering is the credibility:

• Strings, IO and FFI still go through C. 🔭 The runtime membrane is not closed. QUANTA computes and proves; it does not yet own its own edges.
• The memory model is undecided. 🔭 This is a design decision we have deliberately not rushed — get it wrong and every later proof inherits the mistake.
• 570 chapters independently audited, ~59% confirmed genuinely real. 🔬 After 95 repairs, ~59% of the audited census is confirmed real and 60 non-functional stubs were quarantined; what remains weak is the research-scale tier (advanced zk/STARK proof systems, a specialist codec). The gate harness itself is now memory-flat (1.5 GB → 3.4 MB), which is the efficiency thesis embodied in the tooling.

Why it ladders back

A language whose output you can verify byte-for-byte, on any chip, is how correct software gets cheap enough for everyone. That is the abundance argument, made concrete: not "trust us", but "compile it yourself, twice, and check."