LLVM-free · Rust-seeded · Research language

Executable semantics. Checked programs. A compiler stack NAUX can call its own.

NAUX explores proof-gated compilation from a canonical typed core to self-owned native machinery. The current public toolchain is experimental and still uses a Rust/Cargo seed.

Install NAUX Learn View source

hello.nx

~ rite

$msg = "Hello, NAUX!"

!say $msg

~ end

> Hello, NAUX!

Project status

What NAUX is right now

The public learning language and the research compiler share one project, but they make different promises.

Available today

NAUX Learn 0.1.4

A bounded Linux x86-64 learning profile for writing and running deterministic .nx programs without installing Rust or Cargo.

Install the learning profile

Active research

Proof-gated compilation

Typed semantics, partial evaluation, checked lowering, and a self-owned x86-64 path are developed behind reproducible evidence gates.

Inspect the architecture

Boundary

Experimental, not production

NAUX does not yet promise stable compatibility, dependency closure, security-critical suitability, or performance leadership.

Review the source and evidence

Design principles

Why NAUX?

NAUX takes an uncommon path: executable semantics first, aggressive specialization second, and independently checkable evidence at every boundary.

Ritual-first Syntax

Programs use ~ rite entry blocks, $ variables, ^ returns, and ! actions. Explicit blocks, no hidden implicit behavior.

Multi-Engine Execution

AST interpreter, bytecode VM, typed trace JIT, and experimental x86-64 native code — all from the exact same source.

Canonical Typed Core

Surface syntax elaborates to a typed, call-by-value ANF core with explicit effects, regions, and lifetime evidence.

Sovereign Compiler Direction

No LLVM, GCC, or Cranelift backend. NAUX is building its own encoder, object writer, linker, and runtime while openly tracking seed debt.

Futamura Projections

Specialize the canonical interpreter by a known program to produce a standalone residual program, then generate a compiler.

Measured, Not Claimed

Cross-language benchmarks against C, C++, Go, Rust, and Zig with reproducible evidence bundles and strict methodology.

Verified learner corpus

Algorithms written in NAUX—not delegated to host builtins.

Eight representative programs from the 30-exercise S1 corpus. Every example has deterministic input and expected output.

Corpus: 30
Shown: 8
Domains: 7

Basics

Sum an array

Counted input, a bounded loop, and scalar accumulation.

solution.nxNAUX Learn

~ rite
    $n = read_int()
    $sum = 0
    ~ loop $n
        $sum = $sum + read_int()
    ~ end
    !say $sum
~ end

Input

5
3 -2 7 10 4

Output

naux run solution.nx < input.txt

Number theory

Prime check

Trial division terminates at the integer square-root boundary.

solution.nxNAUX Learn

~ rite
    $n = read_int()
    $prime = $n >= 2
    $divisor = 2
    ~ while $prime && $divisor * $divisor <= $n
        ~ if $n % $divisor == 0
            $prime = false
        ~ end
        $divisor = $divisor + 1
    ~ end
    !say $prime
~ end

Input

Output

true

naux run solution.nx < input.txt

Binary search

Search a sorted learner-built collection without a host search builtin.

solution.nxNAUX Learn

~ rite
    $n = read_int()
    $values = []
    ~ loop $n
        $values = queue_push($values, read_int())
    ~ end
    $target = read_int()
    $left = 0
    $right = $n - 1
    $answer = -1
    ~ while $left <= $right && $answer == -1
        $span = $right - $left
        $middle = $left + ($span - ($span % 2)) / 2
        ~ if $values[$middle] == $target
            $answer = $middle
        ~ else
            ~ if $values[$middle] < $target
                $left = $middle + 1
            ~ else
                $right = $middle - 1
            ~ end
        ~ end
    ~ end
    !say $answer
~ end

Input

7
1 3 5 7 9 11 13
9

Output

naux run solution.nx < input.txt

Sorting

Bubble sort

Mutable indexing, nested loops, and an explicit swap.

solution.nxNAUX Learn

~ rite
    $n = read_int()
    $values = []
    ~ loop $n
        $values = queue_push($values, read_int())
    ~ end
    $pass = 0
    ~ while $pass < $n
        $i = 0
        ~ while $i + 1 < $n - $pass
            ~ if $values[$i] > $values[$i + 1]
                $temporary = $values[$i]
                $values[$i] = $values[$i + 1]
                $values[$i + 1] = $temporary
            ~ end
            $i = $i + 1
        ~ end
        $pass = $pass + 1
    ~ end
    $i = 0
    ~ loop $n
        !say $values[$i]
        $i = $i + 1
    ~ end
~ end

Input

5
5 1 4 2 8

Output

naux run solution.nx < input.txt

Graphs

Breadth-first search

An adjacency matrix, explicit queue state, and visited tracking.

solution.nxNAUX Learn

~ rite
    $n = read_int()
    $start = read_int()
    $adjacency = []
    ~ loop $n * $n
        $adjacency = queue_push($adjacency, read_int())
    ~ end
    $seen = []
    $queue = []
    ~ loop $n
        $seen = queue_push($seen, 0)
        $queue = queue_push($queue, 0)
    ~ end
    $head = 0
    $tail = 1
    $queue[0] = $start
    $seen[$start] = 1
    ~ while $head < $tail
        $node = $queue[$head]
        $head = $head + 1
        !say $node
        $next = 0
        ~ while $next < $n
            ~ if $adjacency[$node * $n + $next] != 0 && $seen[$next] == 0
                $seen[$next] = 1
                $queue[$tail] = $next
                $tail = $tail + 1
            ~ end
            $next = $next + 1
        ~ end
    ~ end
~ end

Input

Output

naux run solution.nx < input.txt

Greedy

Coin change

A descending denomination set and repeated greedy selection.

solution.nxNAUX Learn

~ rite
    $count = read_int()
    $coins = []
    ~ loop $count
        $coins = queue_push($coins, read_int())
    ~ end
    $amount = read_int()
    $used = 0
    $i = 0
    ~ while $i < $count
        ~ while $amount >= $coins[$i]
            $amount = $amount - $coins[$i]
            $used = $used + 1
        ~ end
        $i = $i + 1
    ~ end
    !say $used
~ end

Input

4
25 10 5 1
87

Output

naux run solution.nx < input.txt

Dynamic programming

0/1 knapsack

One-dimensional descending-capacity dynamic programming.

solution.nxNAUX Learn

~ rite
    $n = read_int()
    $capacity = read_int()
    $weights = []
    $values = []
    ~ loop $n
        $weights = queue_push($weights, read_int())
    ~ end
    ~ loop $n
        $values = queue_push($values, read_int())
    ~ end
    $best = []
    ~ loop $capacity + 1
        $best = queue_push($best, 0)
    ~ end
    $item = 0
    ~ while $item < $n
        $space = $capacity
        ~ while $space >= $weights[$item]
            $candidate = $best[$space - $weights[$item]] + $values[$item]
            ~ if $candidate > $best[$space]
                $best[$space] = $candidate
            ~ end
            $space = $space - 1
        ~ end
        $item = $item + 1
    ~ end
    !say $best[$capacity]
~ end

Input

4 5
2 3 4 5
3 4 5 6

Output

naux run solution.nx < input.txt

Dynamic programming

Longest increasing subsequence

A quadratic learner implementation with explicit state.

solution.nxNAUX Learn

~ rite
    $n = read_int()
    $values = []
    $length = []
    ~ loop $n
        $values = queue_push($values, read_int())
        $length = queue_push($length, 1)
    ~ end
    $answer = 0
    $i = 0
    ~ while $i < $n
        $j = 0
        ~ while $j < $i
            ~ if $values[$j] < $values[$i]
                $candidate = $length[$j] + 1
                ~ if $candidate > $length[$i]
                    $length[$i] = $candidate
                ~ end
            ~ end
            $j = $j + 1
        ~ end
        ~ if $length[$i] > $answer
            $answer = $length[$i]
        ~ end
        $i = $i + 1
    ~ end
    !say $answer
~ end

Input

8
10 9 2 5 3 7 101 18

Output

naux run solution.nx < input.txt

Complete S1 inventory

30 deterministic exercises across six tracks

Foundations 8

Sum array
Maximum
Count even
Reverse
Factorial
Fibonacci
Euclidean GCD
Prime check

Search and prefix 4

Linear search
Binary search
First occurrence
Prefix range sum

Sorting 4

Bubble
Selection
Insertion
Counting

Graphs 6

BFS
DFS
Shortest unweighted
Dijkstra
Connected components
Topological sort

Greedy 3

Coin change
Interval scheduling
Maximum items under budget

Dynamic programming 5

0/1 knapsack
Minimum coin change
LIS
Grid paths
Subset sum

Compiler architecture

Program flow on the left. Trust evidence on the right.

The diagram separates transformations from the checks that authorize them. A stage existing in research does not mean every surface program reaches it today.

Semantic authority: Typed Core
Native target: x86-64
LLVM in path: None

01
.nx source surface
Available
Span-aware lexing, parsing, diagnostics, and the learner execution surface.
Open contract
OutputParsed surface program
GateSource positions · deterministic diagnostics
02
Canonical Typed Core
Bounded
Typed ANF makes effects, regions, ownership obligations, and observations explicit.
Open contract
OutputVerified Typed Core
GateType · effect · region · ownership evidence
03
Specialization
Research
Binding-time analysis, static evaluation, and residualization remove admitted static work.
Open contract
OutputResidual Typed Core
GateSealed certificate · independent replay
04
Canonical residual SSA
Bounded
A deterministic control/data-flow form becomes the boundary for native lowering.
Open contract
OutputValidated SSA image
GateTranslation validation · correspondence roots
05
Machine IR + x86-64
Experimental
Target planning selects an admitted instruction plan and checked encoding emits bytes.
Open contract
OutputOwned machine-byte capsule
GateMachine verifier · independent decoder
06
Native artifact
Experimental
W^X execution and direct ELF64 experiments run admitted images without LLVM or libc startup.
Open contract
OutputRunner / standalone ELF
GateGate B · containment · dependency inventory

Install NAUX Learn

One supported binary. One command.

NAUX Learn is the small prebuilt profile for writing and running learner programs. Rust and Cargo are not required on the learner’s machine.

Version: 0.1.4
Host: Linux x86-64 GNU
Channel: Experimental

Recommended

Install from the terminal

Available

curl -fsSL https://github.com/x2t8/Naux/releases/download/v0.1.4-learn/nauxup.sh | sh

Downloads the pinned bundle, verifies SHA-256 and its inner manifest, then asks before installing.

01DownloadPinned release asset
02VerifyOuter SHA-256 + manifest
03InstallOwned files + receipt
04Runnaux run file.nx

Installation and platform details Five-minute quickstart

Executable semantics. Checked programs. A compiler stack NAUX can call its own.

What NAUX is right now

NAUX Learn 0.1.4

Proof-gated compilation

Experimental, not production

Why NAUX?

Ritual-first Syntax

Multi-Engine Execution

Canonical Typed Core

Sovereign Compiler Direction

Futamura Projections

Measured, Not Claimed

Foundations 8

Search and prefix 4

Sorting 4

Graphs 6

Greedy 3

Dynamic programming 5

.nx source surface

Canonical Typed Core

Specialization

Canonical residual SSA

Machine IR + x86-64

Native artifact

Install from the terminal