The Eight Axes of Provability

Most systems languages ask you to trust discipline.

Janus is being built around a harder claim:

Write what your code does; the compiler proves what it cannot do.

That sentence is not marketing foam. The verb proves is load-bearing.

A language cannot claim sovereignty because it has a clean syntax, a fast compiler, or a good FFI. Sovereignty begins when the source code exposes enough structure for the compiler, the auditor, and the operator to answer questions that are usually answered by folklore:

Can this mutate a value, only observe it, or consume it?
Can this value cross an actor boundary safely?
Can this call graph touch the world?
Can this binary receive filesystem or network authority at all?
Can this computation fail to terminate?
Can this index, length, port, or scalar be invalid here?
Can this build-time code read the environment or generate artifacts?
Can this function replay with the same result tomorrow?

These questions interlock because real programs interlock. But each one has a primary proof axis. Janus is converging on an unusual answer: make those questions part of the language surface.

Not as comments.

Not as lint.

As compiler facts.

The Category Move

Rust made memory visible and paid ten years of ecosystem tax for it. That was real progress.

But memory is only one axis.

A program can be memory-safe and still ambiently read secrets, make nondeterministic time calls, allocate in a real-time path, leak authority through a callback, block inside an actor, or pretend a partial function is total because the type checker never asked.

Janus treats that as an unfinished revolution.

The emerging Janus model tracks eight orthogonal axes:

Axis	Mechanism	Question the compiler can answer
Memory	Mutable Value Semantics via intents and projections	What does this function do with each value?
Concurrency	Reference capabilities and nurseries	Who may share, send, mutate, or isolate data?
Side effects	Algebraic effect rows	What side effects can this call graph perform?
Authority	Resource capabilities and manifests	Which resources is this binary allowed to touch?
Termination	Total functions	Does this computation finish on all paths?
Preconditions	Refinement types	What must be true before this value or call is valid?
Compile-time	Comptime trichotomy and comptime effects	What runs during build, and with what authority?
Determinism	Deterministic effect discipline	Will the same inputs produce the same outputs under replay?

Two older foundations remain underneath:

Errors — explicit !T error unions.
Numeric conversion — widening, checked conversion, and truncation are distinct operations.

That is the shape of the claim.

The Authority Triangle

The strongest Janus move is not any single axis. It is the way three surfaces line up:

Layer	Question
Effect	What kind of operation is performed?
Capability	Which resource is this code authorized to touch?
Manifest	Which capabilities may this binary receive at all?

Effects are not capabilities. Capabilities are not manifests. Mixing them creates security theater.

The doctrine is sharper:

Effects name the debt. Capabilities authorize payment. Totality proves the ledger closes.

A function may declare !{Net} and still have no network authority. A binary may include code that knows how to touch disk and still be manifest-forbidden from receiving the disk capability. The audit path becomes visible: read the manifest, follow the capability chain, verify the effects, close the ledger.

That is the coherence claim.

Not “safe and expressive.”

Not “Rust, but easier.”

Something sharper:

Janus aims to be the systems language where memory, authority, side effects, determinism, and totality are compiler-visible under one doctrine.

Axis 1: Memory

The memory axis is Mutable Value Semantics.

Values should read as values. Mutation should be visible as intent. References should be compiler machinery, not everyday user syntax.

A Janus signature should say the deed:

func encode(edit buf: [u8], view msg: Message) -> usize do
    ...
end

The programmer says:

view — read this
edit — mutate this exclusively
take — consume this
make — initialize this

The compiler chooses the lowering: copy, pointer, descriptor, noalias, sret, or future projection machinery.

This is the Rust wound, cut differently.

The borrow checker still exists. It just stopped being the programmer’s job.

Hylo’s research validated Mutable Value Semantics in academic isolation. Janus is the first production-targeted language to fuse it with actor capabilities, profile discipline, tensor genericity, and sovereign authority.

Axis 2: Concurrency

Memory safety inside one function is not enough.

Modern systems cross actor boundaries, worker pools, schedulers, queues, and distributed grains. Janus uses reference capabilities to make sharing and mutation explicit:

iso — isolated transferable ownership
val — deeply immutable sharing
ref — local mutable access
tag — identity-only reference

That gives the compiler a vocabulary for actor safety.

It can distinguish a value that may be shared from one that must remain isolated. It can reason about message sends without pretending all references are equal.

Concurrency is not an afterthought attached to memory. It is one of the places where memory either becomes sovereignty or collapses into folklore.

Axis 3: Side Effects

Memory and authority do not tell the whole story.

A function can be memory-safe and still read the clock, touch disk, call the network, allocate, log, receive from an actor, or dispatch a GPU kernel.

Janus needs effects because otherwise profile manifests are aspirational.

An effect row makes world-contact visible:

func fetch_blob(view cid: [32]u8) -> Blob !FetchError !{Net, Alloc} do
    ...
end

The return surface now says three things:

-> Blob — returns a value
!FetchError — may fail
!{Net, Alloc} — may perform effects

Effects are not capabilities. Effects say what kind of debt a computation creates. Capabilities say who may pay that debt against real resources.

This is why the sequence matters:

Effects name the debt. Capabilities authorize payment. Totality proves the ledger closes.

Axis 4: Authority

No ambient authority.

That is not a slogan. It is a language design constraint.

A binary should have a manifest-declared authority surface. The compiler and linker should verify that the call graph never exceeds it.

A function declaring !{Net} does not automatically gain network authority. It must hold the right resource capability, and the binary manifest must allow that authority.

That makes the audit surface small.

Read the manifest. Follow the explicit capability chain. Verify the effects.

Everything else is forbidden by construction.

Axis 5: Termination

A systems language eventually has to answer the ugly question:

Does this finish?

Not every function needs to be total. Kernels, actors, servers, and event loops may intentionally diverge.

But when a function is declared total, the compiler must have enough information to check the claim.

That includes more than recursion:

all branches return, fail, yield, or diverge explicitly;
all effects are handled or declared;
all capability obligations are present;
all make outputs are initialized;
all take paths consume exactly as promised;
all projection teardowns run;
all actor or scheduler suspension points are visible.

Totality is the final accounting layer.

Trying to design totality before effects and capabilities is theater. You prove a toy world, then let the real world sneak in through the handler door.

Janus refuses that order.

Axis 6: Preconditions

Some truths are not types.

A buffer length must be nonzero. An index must be in range. A port must be below 65536. A tensor dimension must match the kernel contract. A cryptographic scalar must be canonical.

Refinement types let the type system carry predicates:

type NonZeroUsize = usize where value > 0

The compiler does not need to become a theorem prover for every possible property on day one. It needs a disciplined path for turning common preconditions into checked facts instead of comments.

That path is deliberately sovereign. Janus will not depend on Z3 or CVC5 as required compiler payload. The first refinement fragment should be native and deterministic: flow facts, interval and congruence analysis, and a restricted Presburger / QF-LIA core. Broader proving belongs on the Janus Sovereign Prover roadmap: a self-hosted prover written in Janus, not a C++ cathedral strapped to the side.

Refinements are the bridge between “this is an integer” and “this integer is valid here.”

Axis 7: Compile-Time

Compile-time execution is not harmless because it runs early.

Build-time code can read files, inspect the environment, generate artifacts, fetch metadata, and poison reproducibility. A sovereign language cannot treat comptime as a playground with root access.

Janus separates compile-time behavior into a trichotomy:

pure compile-time computation;
declared compile-time effects;
forbidden ambient build authority.

If runtime code needs effect rows and capability checks, comptime code needs them too.

Supply-chain attacks do not care that a function ran before the binary existed.

Axis 8: Determinism

Distributed systems do not merely need safety. They need replay.

A function can be memory-safe, authority-checked, and total while still depending on clock time, randomness, scheduler order, filesystem iteration order, floating-point drift, or ambient build metadata.

For sovereign infrastructure, that is not a small leak. It breaks audit, consensus, reproducible builds, deterministic tests, simulation, and forensic replay.

Determinism is the axis that asks:

Given the same declared inputs and the same declared capabilities, will this computation produce the same result again?

This composes naturally with effects. A deterministic function must not perform nondeterministic effects unless they are explicit, isolated, or supplied as values.

Clock time becomes an input.

Randomness becomes an input.

Scheduler nondeterminism becomes a declared boundary.

Build metadata becomes a declared comptime effect.

Janus should not pretend every useful program is deterministic. Servers, actors, schedulers, and entropy collectors live at nondeterministic edges. But the language should let deterministic cores stay provably deterministic.

That is how replay-friendly distributed systems stop being a discipline and become a compiler-visible contract.

Why These Axes Emerged

This was not a feature wishlist.

Each axis was demanded by a concrete crack in the design:

Memory surfaced from aggregate-addressing bugs and the need for honest parameter passing.
Effects surfaced from the profile lesson: :script must not teach a false subset.
Capabilities surfaced from the gap between syscall pledges and user-space resource authority.
Refinements surfaced from predicate holes the other axes exposed.
Termination surfaced from real-time, crypto, compiler, and actor needs.
Compile-time discipline surfaced from the same sovereignty logic as runtime capability discipline.
Determinism surfaced from replay, audit, distributed consensus, reproducible builds, deterministic crypto, and simulation needs.
Structural honesty remains a future discipline: shape requirements should be explicit, but row polymorphism is not yet load-bearing enough to sit inside the eight.
Numeric conversion discipline was already there because silent narrowing is corruption wearing a smile.

The axes were demanded by the structure of Janus itself.

That is why this moment matters.

A category move does not happen when someone invents a clever syntax.

It happens when separate design pressures collapse into one coherent doctrine.

The Doctrine Underneath

The eight axes are not eight gadgets.

They are one doctrine applied repeatedly:

Syntactic Honesty — the source must not lie about memory, effects, authority, failure, or cost.
Revealed Complexity — where the machine matters, the program must expose enough structure for proof.
Mechanism over Policy — the compiler provides mechanisms; profiles and manifests decide policy.

Mutable Value Semantics is the memory doctrine.

Algebraic Effects are the side-effect doctrine.

Resource Capabilities are the authority doctrine.

Totality closes the ledger.

Together they form a compiler-visible contract between programmer, machine, and operator. Effects name the debt. Capabilities authorize payment. Totality proves the ledger closes. Determinism proves the ledger can be replayed.

The Honest State

This is not all implemented today.

The honest status looks like this:

Axis	Status
Memory / MVS	Drafted in SPEC-085 lineage; implementation planning underway
Concurrency	Ratified in the nursery/reference-capability line
Side effects	Drafted in SPEC-090 lineage
Authority	Drafted in the capabilities/manifests line
Termination	Drafted as the final accounting layer
Preconditions	Drafted in the refinement-types line; Z3 rejected, native deterministic prover required
Compile-time	In cleanup through the comptime trichotomy and comptime-effects pass
Determinism	SPEC-096 sketch created; replay/audit axis now grounded

Some axes are ratified. Some are drafted. Some are in cleanup. Determinism now has a SPEC sketch because it is too important to leave implicit.

That matters. Janus should not pretend draft work is shipped work.

But language architecture moves before implementation. If the architecture is wrong, implementation speed only accelerates the wrong failure.

Tonight’s synthesis matters because it gives Janus a coherent target:

A systems language where the important lies are structurally hard to write.

That is the difference between feature accumulation and language design.

The Line

If this article needs one sentence, use this:

Janus lets you write what your code does; then the compiler proves what it cannot do.

If it needs the sharper systems-language claim:

Janus is the only systems language aiming to make memory, authority, side effects, determinism, and totality compiler-visible under one doctrine.

And if it needs the keynote close:

Rust proved programmers would accept compiler-enforced discipline for memory. Janus asks the obvious next question: why stop there?