NAUX North Star

Status: authoritative
Accepted: 2026-07-25
Scope: the destination of the language, compiler, runtime, and toolchain

1. Ultimate objective

NAUX exists to turn executable typed semantics into specialized residual programs and then into native code through a toolchain that NAUX owns end to end.

The destination is uncompromising:

• NAUX must be recognizably different from existing compiler families.
• NAUX must lead performance in the domains where specialization applies.
• NAUX must own its semantic kernel, optimizer, backend, runtime, and tools.
• A normal NAUX release must not require third-party compiler infrastructure, libraries, runtimes, assemblers, object writers, or linkers.
• Correctness and performance claims must be independently checkable.

This is a destination, not a claim about the current implementation.

2. The different path

NAUX does not pursue performance by becoming a frontend for LLVM or by copying the architecture of an existing production compiler. Its primary path is:

Surface NAUX
    ↓ elaboration
Canonical Typed Core
    ↓ binding-time analysis
Partial evaluation
    ↓
Residual Typed Core
    ↓ translation validation
Checked optimization
    ↓
Machine IR
    ↓
NAUX-owned encoder, object writer, linker, and runtime
    ↓
Native program

The interpreter for the canonical Typed Core is executable semantics. Futamura projections turn that semantics into programs and compilers. Proof and evidence checkers protect every transformation that can change observable behavior.

Trace JIT, SSA, equality saturation, region inference, algebraic effects, polyhedral compilation, and hardware specialization are supporting mechanisms. They are admitted only when they strengthen this path.

3. Performance apex

“Top performance” is a measured property, never a slogan.

NAUX graduates a domain only when controlled evidence demonstrates both:

1. generated residual code is within 10% of the best equivalent hand-specialized C or Rust implementation; and
2. NAUX is at least 1.25x faster than a fair generic C or Rust engine on at least one specialization-heavy workload in that domain.

Long-term releases must also keep the geometric mean competitive with the best equivalent native baseline across the active suite. Comparisons must use the same algorithm, numeric contract, inputs, warmup policy, compiler flags, and hardware state.

No result counts when it relies on:

• hidden interpreter or VM fallback;
• undefined behavior;
• relaxed numeric semantics not shared by the baseline;
• an uncontrolled machine;
• missing raw evidence;
• cherry-picked samples.

4. Full sovereignty

The final production trust and execution path is NAUX-owned:

typed core
canonical interpreter
binding-time analyzer
partial evaluator
residualizer
proof and translation checkers
SSA and optimization passes
machine IR
instruction encoder
object/executable writer
linker
runtime
memory manager
standard library
build and package tools
debug and inspection formats

The host CPU ISA, firmware interface, and operating-system syscall ABI are platform contracts, not linked software dependencies. A freestanding target may remove even the operating-system boundary.

External tools may be used temporarily to bootstrap, compare, fuzz, or conduct research, but they must be:

• optional for a normal release build;
• outside the production trusted computing base;
• replaceable without changing NAUX semantics;
• tracked as dependency debt until no longer required.

The current seed build uses rustc and Cargo, and the bridge e-graph path uses egg. Coq, C, C++, Go, and Zig are optional proof, fuzzing, or comparison tools. None may become a permanent requirement of the final NAUX toolchain.

5. Strategic domains

NAUX has three strategic domains:

1. Interpreter/VM — the lighthouse domain for P1 and dispatch elimination.
2. Database/query processing — specialization by schema, plan, shape, and effect knowledge.
3. Numerical computing — region memory, vectorization, affine loop optimization, polyhedral scheduling, and hardware specialization.

The first P1 implementation targets only the interpreter/VM lighthouse. Query processing and numerical computing validate that the architecture generalizes after the semantic and residualization foundations are stable.

6. Futamura path

The projections are product architecture, not decorative research:

• P1: specialize the canonical interpreter by a known program to produce a standalone residual program.
• P2a: specialize the specializer by the interpreter to generate a semantic compiler from Typed Core to Residual Core/SSA.
• P2b: combine that generated semantic compiler with the checked, NAUX-owned native path to produce an end-to-end native compiler.
• P3: generate compiler generators only after P2 is reproducible, inspectable, and useful.

The seed must become minimal, reproducible, independently validated, and discardable. “No traditional bootstrap” does not mean pretending that a trust root never existed; it means the released toolchain no longer depends on the temporary seed.

7. Nauxogenesis

NAUX names its target lifecycle Nauxogenesis:

canonical semantics + specialization kernel
→ projected compiler
→ checked native compiler
→ reproducible generative fixed point

This is not conventional self-hosting under a new label. The compiler remains a derivative of executable semantics. A release may claim Nauxogenesis only when it satisfies the semantic-origin, projection-birth, native-closure, regenerative-closure, dependency-closure, and independent-acceptance gates in docs/nauxogenesis_contract.md.

The first executable established on a target is a declared NAUX Origin Image. Moving that image to a new ISA is architecture genesis. Neither becomes semantic authority or a permanent third-party dependency.

Implementing Core semantics or Surface elaboration in the temporary seed is semantic-foundation work. It is not Projection Birth, generative closure, dependency closure, or Nauxogenesis.

8. Memory and effects

NAUX is region-first and ownership-evidenced:

• proven lifetimes permit stack placement, scalar replacement, arenas, or bulk-free regions;
• RC is a visible fallback for unresolved shared escape, never a hidden hot path foundation;
• certified hot paths can prove that they are RC-free;
• no tracing GC is hidden in the runtime;
• safe code cannot observe physical address, placement, RC traffic, or internal reclamation timing;
• logical identity, alias-visible mutation, effects, and explicit resource lifecycle remain observable.

Algebraic effects are the long-term control abstraction. A known handler may be specialized into direct code. Unknown or effectful work is residualized unless an explicit, reproducible capability allows specialization-time execution.

9. Evidence and trust

The canonical semantic hierarchy is:

1. Architecture Charter and accepted ADRs.
2. Typed Core and language contracts.
3. Canonical Typed Core interpreter.
4. Translation/proof certificates and their independent checkers.
5. Differential, property, fuzz, and regression tests.
6. Backend implementation.

A fast backend that disagrees with the semantic contract is wrong. A generated compiler without provenance is not a NAUX compiler. A performance result without a reproducible evidence bundle is not a claim.

10. Admission rule

A hard or unusual technique enters the active implementation only when it has:

• a direct role in the North Star pipeline;
• a narrow, versioned semantic contract;
• fail-closed behavior outside its proven subset;
• parity or proof evidence;
• observable provenance and diagnostics;
• a controlled performance or capability benefit;
• no permanent third-party dependency.

Difficulty and novelty alone are not sufficient. NAUX takes the uncommon path because that path must produce a result other systems cannot match.

11. Final shape

NAUX is complete only when a developer can provide a general interpreter, schema, plan, or numerical program and receive independently checkable native code at the performance frontier—using a self-generating, self-owned toolchain that requires no third-party compiler stack and has reached its Nauxogenic Fixed Point.