Philosophy & Zen of Naso

The 4 Naso Axioms

These axioms are not guidelines—they are the mathematical bedrock on which Naso stands. Violate them, and the compiler rejects your code. No exceptions.

Axiom 1: Information is Physical

Linear resources ([1]) enforce physical law—quantum no-cloning & entropy conservation are type rules, not runtime checks.

In classical computing, copying a pointer is free. In physics, cloning a quantum state is forbidden. Naso makes this distinction type-theoretic: a [1] Qubit cannot be copied, cannot be implicitly dropped, cannot be aliased. The type system is the physics engine. When you write let q = qalloc(), you are not “allocating memory”—you are asserting exclusive ownership of a physical two-level quantum system. The compiler enforces the no-cloning theorem at the type level. Entropy is not a metaphor here; [1] resources must be consumed exactly once, mirroring Landauer’s principle: erasure has a thermodynamic cost, and Naso makes you pay it explicitly via uncompute or consumption.

Axiom 2: Proofs Over Overhead

Compile-time Z3 proofs replace runtime checks, GC pauses, and dynamic tracing. If Z3 cannot prove it, the machine will not execute it.

Every array bounds check, every null check, every linear usage verification, every quantum uncomputation validity—these are not “safety features” that add overhead. They are proof obligations discharged by Z3 during compilation. The generated machine code contains zero runtime checks for verified properties. A [0] Proof carries exactly zero bits at runtime. A linear buffer inout compiles to a register-to-register move with no bounds checks, no reference counting, no borrow-tracking metadata. The overhead is shifted left—into the compiler, where it belongs.

Axiom 3: Deterministic Execution

No non-deterministic allocation, no hidden background runtime, no GC pauses. Every cycle is accounted for in the type system.

Naso has no garbage collector. No finalizers. No weak references. No background threads sweeping memory. Memory is managed by scope and quantity: [1] resources are deallocated at their single consumption point; [*] resources follow lexical scope (RAII); [0] resources never exist at runtime. Quantum ancilla are returned to $|0\rangle$ by verified uncompute blocks. The execution timeline is fully determined by the source code—there are no “stop-the-world” events, no allocation jitter, no priority inversions from a GC thread. This is not “real-time” as a feature; it is determinism as a consequence of the type system.

Axiom 4: Zero Hidden State

Uncompute intermediate quantum ancilla explicitly or fail the build. Bennett uncomputation is mandatory, not optional.

In quantum computing, every temporary qubit (ancilla) used during computation must be returned to the $|0\rangle$ state before it can be safely deallocated or reused. Failure to do so leaves entanglement “leaking” into the environment—decoherence that corrupts the entire computation. Naso makes this a compile-time requirement: the uncompute { ... } block is not syntactic sugar; it is a verified adjoint generator. The compiler proves (via Z3) that the block’s forward computation is unitary and that its adjoint correctly restores all ancilla to $|0\rangle$. If you omit the uncompute block, or if the block contains irreversible operations (measurement, classical control flow on quantum state), the build fails. There is no “runtime cleanup” for quantum state—physics doesn’t allow it, and Naso doesn’t pretend it does.

The Zen of Naso (10 Aphorisms)

These are not slogans. They are the distilled consequences of the four axioms, written to be internalized.

1. Linear is safe; unbounded ([*]) is suspicious.

   • [1] gives you the compiler’s full attention. [*] says “I promise not to break things.” The compiler believes [1]; it merely tolerates [*].

2. If Z3 cannot prove it, the machine will not execute it.

   • Not “might not.” Will not. The verification condition is the gate. UNSAT = green light. SAT / UNKNOWN = red light. No human override.

3. Memory leaks waste bytes; quantum state leaks break reality.

   • A classical leak is a bug. A quantum leak (dropped entanglement) is a physical error that propagates exponentially. Naso treats both as type errors, but the quantum one gets the stricter error code (NASO-UNC-001).

4. Explicit uncomputation is cheaper than a garbage collector.

   • A GC pauses the world to find garbage. uncompute knows exactly what to clean and when, because the type system tracked it. The adjoint is free—it’s just the forward circuit run backward.

5. Pass by inout grants temporary exclusive mutation rights, not shared confusion.

   • inout x: [1] T means: “I borrow x exclusively, mutate it, and return it. No one else sees it. No one else touches it.” This is stronger than &mut T (which allows reborrowing) and safer than T* (which allows aliasing).

6. Affine loops bound time; QTT bounds space.

   • Polyhedral schedules give you provable iteration counts and dependence-free parallelism. QTT quantities give you provable memory footprints and resource lifetimes. Together, they bound the entire execution envelope.

7. Pointers alias problems; values isolate truth.

   • A pointer is a promise that can be broken. A value (especially a [1] linear value) is a fact enforced by the type system. Naso defaults to values. Pointers exist only in std::mem for FFI, and they carry [1] or [0] quantities.

8. A compile-time diagnostic today prevents a physical decoherence disaster tomorrow.

   • The cost of a NASO-UNC-002 error at compile time is seconds. The cost of the same bug on a 1000-qubit processor is a failed experiment, wasted beam time, and potentially damaged hardware. Naso makes you pay the small cost upfront.

9. No hidden runtime, no dynamic tracing, no surprises.

   • What you see in the source is what executes. No JIT compilation. No dynamic linking surprises. No reflection. No Any type. The binary is a pure function of the source and the target triple.

10. Hardware is physical—your type system should be too.

    • Qubits are physical. Cache lines are physical. DRAM rows are physical. ALU pipelines are physical. A type system that ignores physics (aliasing, copying, dropping, unbounded loops) is a fiction. Naso’s type system models the hardware: linear for unique ownership, bounded for finite resources, erased for proofs, polyhedral for structured parallelism.

Explicit Non-Goals

Naso achieves its guarantees by refusing to be certain things. This is not omission—it is architectural discipline.

Frequently Denied Requests (FDR) Callout Box

Closing Thought

“The purpose of a type system is not to prevent errors. The purpose of a type system is to make invalid programs unrepresentable. Naso extends this principle to quantum state, hardware topology, and physical law.”

— Naso Design Manifesto, §1.0