§ 90 · non-normative · depth 0 · edit the source

Rationale

Non-normative throughout. Nothing here constrains an implementation.

This section exists because a design document that lists only advantages is marketing. For each inversion: what HolyC did, what Nether C does, and what that cost.

90.1 The inversions

The command line is the compiler → there is no `run`

HolyC compiles and executes each top-level statement as it is read. The shell, the REPL and the build are one act, and the result is a system with extraordinary immediacy: you type, and the machine has already done it.

Nether C moves all of it to the other side. Burial is partial evaluation, and the artifact is the residue.

What it cost. Immediacy. There is no REPL and there cannot be a good one, because the thing a REPL is for — see the effect now — is precisely what this language refuses to do. The Necropolis playground is the compensation, and it is a worse experience than a REPL for the things a REPL is best at.

A bare string prints → a bare expression deposits

The syntax is preserved exactly; the semantics are reversed. "Hello\n"; is still a complete statement, and it still means this value matters. It simply no longer reaches anybody.

What it cost. printf debugging. The first thing every programmer does in a new language is print something, and in Nether C that takes two commands instead of one. This is the single largest ergonomic tax in the design, and it is charged on the first thirty seconds of every newcomer's experience.

The defence is that it buys the strongest property in the language: a program holds no capability that reaches a log, so it cannot leak to one. Whether that trade is worth it is genuinely arguable, and if Nether C fails to find users, this is the most likely reason.

The Oracle → stratum 7

Terry's random number generator was a channel: entropy arriving from above, the highest thing in the system. Nether C puts randomness at depth 7 — nearly the deepest thing there is — because it is the one act that makes a program impossible to re-derive.

This is the cleanest inversion in the design. The same mechanism sits at opposite ends of the same axis, for reasons each system states outright.

What it cost. Nothing, in engineering terms. Everything, in the sense that it is the point where Nether C is most obviously arguing with TempleOS rather than merely differing from it. That is intentional and it is meant respectfully.

Ring 0 for everyone → nine strata

TempleOS gives every task every privilege over all of memory at all times, and gets a system that switches tasks in half a microsecond and is a joy to program. Nether C partitions authority into a lattice and records the partition in every type.

What it cost. Speed of expression. In HolyC you write what you mean. In Nether C you write what you mean, discover it is at depth 5, and go back to add a descend. Depth inference is what keeps this from being intolerable, and if inference is not good enough the language is not usable.

Everything mutable → nothing mutable

Both systems share everything. TempleOS lets every task write to it; Nether C lets none write to anything.

What it cost. Every algorithm that wants an in-place update. §5.4 permits building an aggregate before it is first read, which covers construction but not, say, a hash table that is updated a million times. A Nether C program that needs one will be slow, and the honest answer today is that such a program should be written somewhere else and called at stratum 8.

DolDoc → the ledger graph

TempleOS's file is alive: source, documentation, UI and runnable macros in one illuminated hypertext, with sprites drawn inline. It is the most charming thing about the system.

Nether C makes the text disposable and the graph canonical. The source is one rendering of the program; the trace is what actually exists.

What it cost. Charm, so far. The ledger graph is a better substrate for diffing, provenance and reproducibility, and it is currently much less pleasant to look at than a DolDoc file. The Necropolis exists to close that gap and has not yet been built, so this comparison is not yet one Nether C wins.

640×480 forever → the Decay Rule

Terry fixed the dimensions of the system by covenant and never changed them. Nether C's counterpart is that the trusted core may only ever get smaller — checked in CI, recorded in .decay-ceiling.

A fixed constraint and a monotonically decreasing one are both ways of refusing to let a system sprawl. The second is more demanding.

90.2 Rejected alternatives

The Orpheus rule: two rejected forms

Scope re-stain. look raises the depth of the whole enclosing scope to the shade's origin. Mythologically exact — turning around costs you everything — and it produces errors nobody can read: one look deep inside a function poisons every caller, and the diagnostic points at the caller rather than the cause.

Binding taint. Only the bound value takes the depth. Tractable, familiar, and it reduces shade to a newtype: if looking is free, nothing has been carried.

The rule in §1.6 — you may only look by going back down — was chosen because it is a local check rather than a propagation, gives an error that names the exact fix, and keeps the myth intact. Orpheus could have kept her; what he could not do was look on the way up.

proof/orpheus.py checks both halves of [LOOK]'s premise d ∈ δ:

Sufficiency: d ∈ δ implies both max(d, d′) ≤ max(δ ∪ g(s)) when d′ ≤ max(δ ∪ g(s)) (preserving §2.4's ambient soundness) and {d} ⊆ δ ∪ g(s) (preserving per-stratum capability confinement).
Necessity and the non-interval counterexample: for a closed shade value (g(s) = {}, d′ = 0), capability confinement {d} ⊆ δ is equivalent to d ∈ δ, whereas the numeric ceiling max(d, 0) ≤ max(δ) of §2.4 alone is equivalent to d ≤ max(δ). When δ is not a downward-closed interval — for example d = 3 (disk) and δ = {0, 5} (net) — 3 ≤ max({0, 5}) holds (3 ≤ 5) while 3 is not in {0, 5}. Requiring d ∈ δ rather than d ≤ max(δ) is therefore stronger than §2.4's numeric ceiling alone and exactly what §1.6's per-capability rule requires. Dropping the premise altogether (binding taint) fails even §2.4 (d = 3, d′ = 0, δ = {0}), and pushing {d} ⊆ dƒ onto the enclosing function (scope re-stain) combined with [APP]'s dƒ ⊆ δ_caller still forces d ∈ δ_caller at every call site.

What a grant gates: a call, or a depth

§6.1 said burial could evaluate an expression "when the expression's depth is within the granted capabilities". Read as written, that leaves a whole class of expression with no outcome. descend disk { 1 + 1 } under no grant is at depth 3 and not within nothing, so burial cannot evaluate it; §6.3 forms a hole only from a prelude call with finished arguments, and there is no call; and §6.4 starves only what waits on a hole, and there is none. It has not collapsed either — it produces 2, and will the moment anybody asks. Three rules, no answer. look on a shade that already has a value is the same shape.

The alternative was to make it a fourth outcome: an expression that is deep, ungranted and not a call is neither evaluated nor a hole, and §6.5 would say it residualises as the descent written out, since there is nothing inside it to reduce. That is coherent and it buys nothing. The burial would be refusing to fold arithmetic on the grounds that somebody once wrote descend disk around it, and the residue it produced would fold on the next burial for a reason unrelated to anything the world said.

So a grant gates a call. What is owed to the world is a question, and an expression that asks no question is not owed anything.

That has a consequence for the Orpheus rule that is worth stating rather than leaving to be discovered, and §1.6 now states it. look is checked and never granted: it costs the writer a descend and costs the operator nothing. The binding-taint form rejected below was turned down partly because "if looking is free, nothing has been carried", and looking is free of the world under either form. What is carried is not the cost of opening — it is that a deep value can be held, passed and stored at depth 0 without staining what holds it, and that opening it names the stratum again where a reader can see it.

What it cost. A sentence admitting that one of the two escapes in the lattice is a discipline rather than a gate. That reads as a weakening and is not: the witness was written when the value was fetched, by whoever held the capability then, and nothing about looking at it later can un-write that.

Stratum 8: refusing foreign code

The purer design has no stratum 8. Every value in every trace would then have a complete history, unconditionally, and every claim in this specification could drop its qualifier.

It was rejected because a language that cannot call C cannot be adopted, and an unadopted language proves nothing about whether its ideas were good. The quarantine in §1.7 is the compromise: foreign code is permitted, and a trace that used it is permanently forbidden from claiming to be replayable.

This remains the weakest part of the design.

Failure: three rejected forms

Exceptions. Rejected outright. Unwinding presumes a stack that exists at a single moment, and burial has no such moment — an expression may be evaluated now, residualised, and finished a week later by somebody else's exhumation. There is nothing to unwind to.

rescue e else f, catching a collapse. Superficially the most elegant option: a collapsed node would be a first-class thing in the trace, so expose it and let a program handle it. Rejected for two reasons. It makes bugs catchable, and a bug that can be caught is a bug that will be ignored. Worse, it makes evaluation order observable — whether rescue fires depends on how far burial got before it collapsed, which is exactly the kind of dependence §6.2 exists to forbid.

Nothing, and say so. Declare failure a burial-level diagnostic and put recovery outside the language. Honest, and fatal: a build system that cannot say if this file is missing, generate it is not a build system, and build systems are the case that motivates the whole design.

What was chosen instead splits the question in two. A no from the world is an answer and gets a value; a mistake in the program is a collapse and gets a stopped burial. The cost is a check at every world-touching call site, which is the bargain C has always offered and which this language is in no position to improve on.

One word for starving and for collapsing

An earlier draft used starve for both: for an expression waiting on a hole (§6.4) and for one that can never produce a value at all (§9.9). §10 defended the merge — "deliberately given one name because both stop a burial" — and that reason was not true of the first one. §6.4 says a starved expression is residualised and waits. It does not stop anything; it is the ordinary outcome, and it is what the whole language is for.

Two other ways out were available.

Rename §6.4's instead, and keep starve for the fatal case. Rejected because the word is already spent: starved means waiting on something somebody else must supply in this project's vocabulary table and in the roadmap's own item status, and a term that means one thing in the tooling and its opposite in the specification is worse than either.

Leave them merged and rely on context. Rejected on contact with the implementation: nether-bury has to tell them apart to report either, one is a Halt and the other is not, and a reader of §9.9 who has not read §6.4 comes away believing burial stops whenever anything waits.

So the fatal one is a collapse. It reads in the register the rest of the language is written in — a burial that hits one caves in — and it leaves starve meaning the one thing it means everywhere else.

A shade's origin: in the value, or only in the type

§5.3 once said both things at once. Equality is structural — two values are equal exactly when their encodings are — and then, one paragraph later, that two shades are equal when their underlying values are. §7.1 encodes a shade as an origin byte and the cairn of what it holds, so a shade of the same bytes from stratum 3 and from stratum 5 were unequal by the first rule and equal by the second.

The other way out was to drop the origin byte, making Shadeᵈ⟨T⟩ encode exactly as the cairn of what it holds and leaving the origin a fact the type carries. Rejected, and not only because §7.1 is frozen. §1.6 says a shade MAY be stored, and the only place a Nether C value is stored is the ledger. A shade read back out of the ledger with no origin has lost the one thing that makes the Orpheus rule checkable, and look on it could not be typed at all. The origin is not metadata about the shade; it is half of what a shade is.

What that costs is the sentence in §1.5: seal on a shade no longer reaches through to the value inside. It names the shade. That is the tighter rule anyway — a shade is opaque, and reaching through an opaque thing for a name was a small hole in it — and it takes nothing away, because seal e is legal at any depth and can simply be written before the shade.

`sizeof`, which had no answer

§4.5 carried "sizeof" "(" type ")" as a production from the first draft, inherited from C along with the rest of the surface, and nothing anywhere said what it evaluated to. Burial residualised it, which was the only honest thing left to do with a form that has no value.

Two ways to give it one were available.

The length of the canonical encoding. Precise, and a different question from the one sizeof is asked: §7.1 gives Bytes a length prefix and then the bytes, so the answer depends on the value and not on the type. sizeof(Bytes) would have no answer even then, and sizeof of a value is a different operator wearing the same name.

A fixed size per type. That means inventing a memory layout, and the whole of the C reason for sizeof — how much memory to ask for — does not exist here. There is no pointer type, no array decay and no allocation. A layout invented only so that one operator can report it is a fact about nothing.

So there is no sizeof. len answers the question people reach for it to ask. The word stays reserved (§3.4) because a C programmer will write it, and an error that names len is worth more than a program that binds sizeof to something of its own.

Normalising text in the ledger

An earlier draft had the ledger encode Str over its NFC form, so that two spellings of one string could not produce two cairns. It was removed while freezing §7.1, for two reasons.

The first is a matter of what a content-addressed store is for. If the store normalises, then cairn(s) is not the name of s; it is the name of something the store decided s ought to be. A program that writes a decomposed string and reads back a composed one has been lied to by the one component whose entire job is not lying about bytes.

The second is that normalisation belongs where the ambiguity is actually a problem: identifiers. Two spellings of a variable name must resolve to one binding, and §3.3 makes the lexer responsible for that. Nothing below the lexer needs an opinion.

It also removes a dependency — full NFC is a megabyte of Unicode tables — but that is a consequence of the decision, not the reason for it. Had the argument gone the other way, the tables would have been the right thing to add.

Inferring the type of a block-level binding

§5.6 used to say types were inferred within a function body. §4.2 has one let_decl production and it begins with a type, so the binding §5.6 described could not be written at all.

The fix would have been a second statement form. n = 0; is unavailable — §5.4 keeps assignment, so that spelling is already taken and the two would be indistinguishable — which leaves a keyword, let n = 0;, and a language with two ways to bind a name.

It was rejected for what it buys: four characters, in exchange for a keyword, a second binding form, and a reader who has to know which one they are looking at. Nether C is a C dialect and C writes the type. The language already asks for types on every other binding, and making one of them different is the kind of exception that has to be remembered rather than understood.

What the rule became is a better sentence than the one it replaced. Types are written; depths are inferred. A type is a fact about what a value is, which the writer knows. A depth is a fact about where it came from, which is derived from everything it touched and is exactly what a person gets wrong.

Struct literals, and forbidding assignment outright

§4.4 had an assign production and a for step that nothing could reach: §5.4 said a binding may not be reassigned, and §4.2 required every let to have an initialiser, so there was no way to write a struct value and no way for for (I64 i = 0; i < n; i += 1) to advance its own counter. Three constructs in the grammar with nothing that could produce them.

A struct literal in primary was the obvious fix: make aggregates ordinary values, Header { len: 3, tag: b"nc" }, and drop §5.4's build-then-seal discipline entirely. It is a smaller grammar and a cleaner story. It was rejected because it fixes one of the three: for still cannot step, assign is still unreachable, and a language that cannot advance a counter has no loops worth the name.

Forbidding assignment outright — remove assign, remove the for step, remove §5.4's example — was the honest minimum, and it leaves a language with while and manual recursion and nothing else. The inversion does not require that. What TempleOS let every task do was write to shared, addressable, permanent memory; a counter in a block is none of those.

What was chosen draws the line at the ledger. A local may be assigned until it is named, and naming it is exactly the moment its cairn exists. That keeps §5.4's original sentence — "once a value has been read, its cairn exists, and nothing can change what a cairn names" — which turned out to be right all along, and makes all three constructs reachable for one reason rather than three.

The cost is that "there is no mutation" stops being true as a flat statement and becomes true only of the ledger. That is a worse sentence and a better rule.

Recording the fuel budget in the trace

§8.2 used to require that the budget be reported in the trace, "because a trace buried under a different budget is a different trace". It is not, and it cannot be: running out of fuel produces a halt rather than a trace, so a budget either lets the burial finish — in which case it changed nothing — or there is no trace to have changed.

The rejected alternative was to add the budget to Node::Trace anyway and justify it differently: that a trace should record the conditions it was made under even where they did not bind. There is a real argument for it. If a later burial of the same residue under a smaller budget halts where the first did not, somebody will want to know what the first one was allowed.

It was rejected because the cost is concrete and the benefit is speculative. Adding a field to Trace changes what an existing tag means, which bumps the domain separator (§7.2) and renames every value ever stored. Paying that to record a number that provably did not affect the result is the wrong trade, and if the diagnostic case turns out to matter it can be served by the rite's own output rather than by the artifact.

Calling a nullary function without parentheses

HolyC does not need them: Dir; calls Dir. The first program in this specification was written as demand greet; for a year on the strength of that memory, and it does not call anything — §4.5 requires call_suffix, so a bare identifier is the function itself. The body never ran and nothing was deposited, and nobody noticed because nothing could run at all.

The tempting fix is the grammar: let a bare identifier of function type call itself. It was rejected because it reintroduces exactly the ambiguity the rest of the language spent its budget removing. greet would mean the function in one position and its result in another, and the reader would have to know the type to know which — in a language whose whole proposition is that a value's type tells you what it cost.

It would also make seal greet ambiguous in a way that matters: the cairn of a function and the cairn of what it returns are different names for different things, and there would be no way to write the first one.

What it costs is two characters and a small loss of the homage. HolyC's parenthesis-free call is one of its most characteristic gestures and this is a place where Nether C simply does not follow it.

A residue as nodes

§6.5 used to say the residue was "every node that could not be reduced, plus the holes, plus the provenance edges between them", and §7.3 listed six node kinds, none of which can hold a branch, a loop, a binding or a block. A residue routinely contains all four. The two sections could not both be right.

The rejected fix was to add node kinds until a residual program fitted — Branch, Loop, Bind, an unreduced Apply. It has one real argument in its favour: §6.6 counts nine hundred and three nodes for a program with a single hole in it, which is the residue being counted, so the summary already assumed this reading.

It was rejected because it makes the ledger hold two unrelated things in one vocabulary. A node records something that happened — this was applied to that, the world said this, at this place in this file. A residue is something that has not happened. Encoding both as nodes means every consumer of a trace has to know which kind of node it is looking at, and the distinction is not visible in the type.

What was chosen instead: a residue is a program, a program is source, and source is Bytes. It costs a print and a parse on every re-burial, which is real work that the node encoding would not have needed. It buys a Trace whose parts each mean one thing, and it means the staging law is stated over something that demonstrably round-trips — the printer has a proof that lowering what it printed gives back the same program, node for node.

Bumping the domain for any change at all

§7.2 used to say that changing the encoding changed the domain separator, full stop. Taken literally that made the format unable to grow: assigning a tag that had never meant anything would have renamed every value ever stored, including all the ones the new tag has no bearing on.

The rule now distinguishes two things. Changing what an existing tag means bumps the domain, because a byte string that decoded to one value now decodes to another and calling both by the same name is a lie. Assigning a tag that was previously rejected as unknown does not, because no byte string changes meaning — the ones that decoded still decode identically, and the ones that were refused are simply refused less often.

What this gives up is a very simple sentence. "Any change bumps the domain" can be checked by looking at a diff; "any change to what an existing tag means" needs somebody to think about which kind of change they made. That is a real cost and it is paid by whoever reviews the next format change.

It was taken because the alternative was worse in a way that only shows up later. A format that cannot add a tag without discarding history is a format that will be forked rather than extended, and then there are two.

Writing our own cryptography

The repository has no third-party dependencies. Not in Rust, not in the site, not in the graphics: site/gfx.py contains a GIF89a encoder, an LZW compressor, a PNG encoder and a bitmap font rather than importing any of them, and the argument each time was that the part actually needed was smaller than the cost of the dependency.

That argument does not survive contact with §7.2, which specifies blake3.

A hash function is not an encoder. An encoder that is subtly wrong produces a file somebody notices. A hash function that is subtly wrong produces cairns that look fine, verify fine, and collide — and the failure surfaces years later as two different values with the same name, in a store nobody can now audit, underneath every reproducibility claim in this document. Timing behaviour, buffer edge cases and the compression-function rounds are exactly the places where hand-written implementations go wrong quietly.

So the rule is narrower than "no dependencies", and it is worth stating precisely, because the broad version is the kind of principle that feels good until it costs something:

Write your own encoders, parsers, renderers and formats. Do not write your own cryptography.

blake3 is a permitted dependency. Every addition after it needs its own entry in this section.

This is also consistent with the Decay Rule rather than in tension with it. The ceiling counts the lines this project is responsible for, and three hundred lines of hand-rolled hashing would be three hundred lines of exactly the code nobody should be reviewing here.

Unicode, and the line the rule is actually drawn on

§3.3 needs two things Unicode is the authority for: which code points start and continue an identifier, and NFC. Working out how many lines the part actually needed would be, as the rule requires: the XID properties are about seven hundred ranges, and NFC is two thousand decomposition mappings, nine hundred combining classes and an exclusion list. Two hundred lines of algorithm and forty-five hundred lines of data.

The failure mode is blake3's. Two identifiers that should compare equal and do not are a program that resolves one name to two bindings, quietly, and §3.3 already says so in as many words.

The Decay Rule settles the rest. .decay-ceiling counts the code every guarantee rests on, and four and a half thousand lines of UCD is not that code: it is not ours, we would not read it, and it changes once a year when Unicode publishes. Putting it in the count would mean every future commit measuring itself against a number that is mostly somebody else's data. Generating it at build time moves the lines and not the problem.

What it cost, measured rather than estimated: in the module web/necropolis/ downloads, the tables are the largest single thing there is. The data section is 141 KB on the wire's far side and 67 KB compressed, of which about 10 KB is every diagnostic this project writes and the rest is perfect_hash, decompose and lookups. That is 44% of what a browser downloads to bury a program, spent on a correctness property most programs never exercise — and it is still the right trade, because the property it buys is that two spellings of one name cannot become two bindings, quietly. The alternative is a subset of somebody else's data, which is the thing the rule above refuses. tests/wasm/run prints the breakdown on every build so that this stays a decision rather than a discovery.

So unicode-ident and unicode-normalization are permitted, the language pins Unicode 16.0, and the rule the three of them share is worth stating because "no dependencies" was never quite it:

A dependency is admissible when what it holds is data, or a construction, that somebody else is the authority for. It is inadmissible when what it holds is behaviour this project could write and should understand.

blake3 is the first kind. Unicode is the first kind. A markdown renderer, a GIF encoder, an argument parser and a web framework are the second kind, which is why this repository has written four of those and imported none.

Fuel and `opaque` as command-line concerns

The obvious cheap answer: make the fuel budget a --fuel flag and the barrier a --no-inline list, and keep both out of the language.

Rejected because a trace buried under a different budget is a different trace. If the artifact depends on it, it is part of the artifact, and a thing that is part of the artifact has to be visible in the source that produced it. A build that succeeds on one machine and exhausts on another because somebody's shell alias differed is precisely the class of failure this language exists to make impossible.

The cost is a keyword. opaque is the only construct in Nether C that exists to make the compiler do less, which is an odd thing to have to teach, and it will be the first thing a newcomer mistakes for an optimisation hint.

Leaving a starved call as the call it was written as

The first implementation of burial did this. A call whose body could not be finished residualised as the call, and the reduction the body had already gone through was thrown away. It is a defensible rule: the residue is smaller, it reads like the program somebody wrote, and it is never wrong — burying the residue simply does the work again.

Rejected because it makes a first projection impossible, and a language whose whole claim is that burial is partial evaluation cannot leave the projection out. Measured on this repository's own bootstrap — lib/interpreter.nc joined with lib/value.nc and lib/evaluate.nc, buried against build.nc with read("main.nc") unanswered — the residue was 1,163 lines whose only demand was interpret(b"…the whole of build.nc…"). The 4,993,540 steps that had read and checked the guest were in the trace and not in the residue, so the next burial spent them again. Nothing had been specialised to anything.

The cost is size, and it is not small. The same burial under §6.5's rule mints one function per starved call site — 21 of them, and a residue of 1,478 lines against 1,163 — because each carries the constants it was specialised to, the guest's source among them. An implementation can drop the bindings nothing in the residual body reads, and should; what it cannot do is drop the shape, and a programmer who wants the smaller residue back has to ask for it with opaque.

A `Bytes` literal without a byte escape

There was no \x until demand b"\u{e9}" was found to print as a residue that lowers to a different program. Three ways not to add one were considered.

Let a bytes_literal hold raw bytes. The obvious answer, and the one C takes. Rejected because §3.1 says a source file is UTF-8, and a lone 0xe2 is not. Relaxing that for the inside of one literal means a lexer that stops being able to work in str, an editor that shows the file as damaged, and a diff nobody can read.

Let \u{…} mean a byte inside b"…". No new syntax, and the printer already writes it. Rejected because the same escape would then mean a scalar value in one literal and a byte in the other, and \u{1f480} would be legal in one and an error in the other. An escape that means two things is read wrongly once and then trusted.

Take the variable-length \x. C's spelling, so it would look familiar. Rejected because b"\xeff" is then one literal or two depending on how far the reader looks, and it is a bug people have actually written. Exactly two digits has one reading.

The cost is a fourth thing to know about literals, and an asymmetry: \x is admissible in b"…" and not in "…". The asymmetry is the type's, not the lexer's — a Str is UTF-8 and a Bytes is not — but it still has to be taught.

One number for how far a value went and for what you may do

δ was a number: the deepest stratum whose capability is currently held. [APP]'s premise was dƒ ≤ δ and [DESCEND] raised δ to max(δ, s(κ)), so the same total order carried two unrelated jobs — how far a value's history reaches, and which capabilities are in hand.

It does not survive the second one. disk! is stratum 4 and net is 5, so inside descend net the premise 4 ≤ 5 held, and the write in §1.3's second sample was accepted. A reader auditing that program's descents would have been told it touches the network. §9.1 fixes the capability names precisely so that reading them is an audit; an order that implies one permission from another takes the audit back. §1.8 had already said the ordering was how much of the world you have disturbed and called the 4-before-5 placement "arguable" — fine for comparing two histories, and not a thing to rest authority on.

Three ways to keep one number were considered.

Declare the subsumption and mean it. Say in §1.1 and §8.2 that a grant at stratum n grants every capability at or below it, and that --grant net is --grant disk! as well. Honest, and it leaves no invocation that says fetch this URL and touch no files — which is the case the whole apparatus exists for. §8.3.2 spends a subsection bounding which host net may reach; under this reading it would be a fence beside an open gate.

Split the two gates. Keep dƒ ≤ δ as a static declaration of reach and put the real authority in the grant, so descend net { write(p, c) } checks and then leaves a hole because disk! was not granted. It is sound — nothing happens that was not granted — and it costs the property that made the names worth fixing: the program text stops disclosing what the program reaches, and only the invocation knows.

Let a function ask for at most one capability. Keep the arrow's dƒ a number and read the premise as membership, κ(dƒ) ∈ δ. A body that calls two prelude functions bare at different strata then has no derivation and must descend for one of them itself. Sound, no grammar change, and an exception that has to be remembered rather than understood — the same objection that killed a second binding form earlier in this section.

What was taken instead: δ is a set of strata, dƒ is a set, and the premise is dƒ ⊆ δ. The capabilities are in bijection with the strata, so a set of one is a set of the other and no new object enters the calculus. [LOOK] gets the sharper rule as a consequence — d ∈ δ, so a shade out of stratum 3 opens under descend disk and not under a deeper descend net, which is what going back down always said and what a comparison of two numbers did not enforce.

What it cost. A second spelling in the grammar: @{3,5} for a signature that asks for two, where a single digit used to cover everything (§3.5). A reader who knew δ as a number has to relearn it. And a program that reads and writes the disk now nests two descents where one used to do, since disk no longer arrives with disk! — which is the cost being paid for, stated as a cost.

Also rejected: letting descend take a list, descend disk, disk! { … }, to buy that nesting back. It is a grammar change for an ergonomic one, nesting already says it, and §1.3 is clearer when one descend means one capability.

One hole for every identical call, whatever stratum it was

The rule §6.3 shipped with was simpler and read better: two holes with identical calls in one trace are the same hole, and the justification given for it was a read — asking the same file for its contents twice is one question.

Rejected because it ranges over the other half of the lattice, where it is false. Two posts to the same address with the same body became one message and one witness, and §1.8 spends a section arguing that a write is deeper than a read precisely because it cannot be taken back. Two draw(8)s became the same eight bytes, which makes the one prelude function §9.7 calls the only source of nondeterminism in the language a pure function of its argument within a trace. Neither was noticed because the rule was written with a read in front of it and proved with a read.

The cost is that §6.3 is now two sentences where it was one, and that a call is no longer a name for a question — it is a name for a kind of question, which is why the answers to one have to be ordered. Addressing an answer by the span that asked would have kept the one-to-one and was rejected too: a span is a fact about one text, and §6.5 requires a residue to be printed and lowered again, which gives every hole in it a new one.

Evaluation order as the implementation's business

§6.2 left the order inside a demand unspecified and asked only that it be deterministic for a given source and capability set. That is the usual and usually correct thing to say: burial is pure, nothing a program can write observes the order, and an implementation that wants to evaluate arguments right to left should be allowed to.

Rejected because burial writes the order down. A trace carries the holes in the order they were discovered (§7.3); a shared hole keeps the span of the first place that asked (§6.3), and §6.3 calls which place that is "a fact about the program rather than about the implementation"; and a fuel budget runs out at whichever node was reached first, which §6.4 requires two implementations to agree on. Three sentences in three sections all rest on an order that a fourth declined to fix. The total fuel a finished burial spends is the same either way, which is why this survived: it is visible only under a budget that binds, and under a budget that binds is the case §6.4 exists for.

The alternative was to weaken §6.4 to what §6.2 supported — fuel is deterministic for one implementation, the way the frame and space limits three paragraphs below it already are. Rejected because those limits decide whether a burial finishes, and §6.4 goes on to say that two implementations "MUST NOT disagree about the result when both of them finish". Order is not like that. It is in the result.

What it costs. An implementation may no longer reorder evaluation for speed where the reordering could change which node is reached first, which is most reorderings. A parallel burial — 0204 — has to discover holes, keep spans, and charge fuel as though it had run sequentially, and produce the serial trace rather than whatever order the threads finished in. That was already true of the hole order; it is now also true of the budget.

The deposits as a set

§7.3.1 did not say whether a trace's deposit list could hold the same cairn twice, and a set was the cheaper reading: the deposits are the record of which values were deposited and where, a repeat adds nothing a reader did not already have, and a trace then does not grow with a loop's trip count.

Rejected because §8.4 calls lamp "how a program's output is read", and output that swallows repeats is not output. for (I64 i = 0; i < 1000; i += 1) { "tick\n"; } reading as one tick is a bug anybody would report, and the reason is the one §6.3 gives for not merging two identical sends: a trace that describes fewer things than the program did is a trace that lies about what was done. A set also means a program cannot deposit the same value from the same span twice, which is a surprising thing to forbid in a language whose only output channel this is.

Neither reading was obviously wrong, and leaving it unsaid was: the list is part of the Trace's encoding, so the two readings give the artifact two different cairns, which is what §7.1 is frozen to prevent. The implementation had already chosen both — burial recorded four deposits for the loop above and lamp printed one tick — which is what an ambiguity looks like from inside.

What it costs. Thirty-two bytes in one list per turn of a loop that deposits. Not a node each: the Deposit is one node however many times the trace names it.

The deposits as a set

What it costs. Thirty-two bytes in one list per turn of a loop that deposits. Not a node each: the Deposit is one node however many times the trace names it.

The disk root as the implementation's, and a reach that names a port

Two smaller choices in §8.3, which grew a fourth subsection when the disk turned out to be the one bounded capability the invocation could not bound.

Leave the root to the implementation. It is what every version of this document did, and there was a case for it: §09 talks about paths and not about filesystems, the bound is an operational concern, and the one implementation here already had a root that nothing may climb out of. Rejected because the bound existed and was undeclarable, so an operator could not say where a burial may read and two implementations could answer read("main.nc") differently while the hole's call was byte-identical. A reproducibility claim that touches a filesystem touches it exactly there.

A root that repeats, resolved as a search path. --load repeats and takes the first object that has the symbol, and reads could work the same way. Rejected because a write could not: a path does not name its root the way a URL names its host, so two roots leave every written path ambiguous and the invocation would need a second flag to say which one a write lands in — a flag to disambiguate a flag. One root, and a build that needs two things in one place puts them there.

A bare --reach host meaning the scheme's default port. Tighter, and it matches the standard the rest of the section keeps: a grant states its bound. Rejected because the thing being declared is a party rather than a service, and an operator who trusts example.com over 443 has said something about example.com rather than about 443. The cost is real and §8.3.2 now states it instead of implying it: a bare host permits every port on that host, and the program chooses which.

Leaving an undecided arm alone

§6.5 used to stop at a branch. An if whose condition waited on the world residualised with both arms untouched, on the grounds that reducing one would be evaluating something no demand requires and §6.2 forbids that.

It reads as the conservative choice and it is the expensive one. §6.2's reason is stated in §6.2: an undemanded expression could reach the world and leave a witness for something the program never asked for. That is a reason about reaching the world, not about reducing — and a partial evaluator that stops at the first branch on an unknown value stops immediately, because an interpreter's first act is to branch on the thing it was given. The projection this language is named for was being given up to protect a guarantee that folding arithmetic does not threaten.

Three ways to keep the branch sealed were considered.

Leave it. Defensible, and it makes §6.5's "what this is for" paragraph claim something the rule does not deliver: bury an interpreter and you get the interpreter back, specialised up to the first if. The first Futamura projection is the section's own stated purpose and this is the rule that prevented it.

Speculate under a separate, smaller budget, so that a divergent arm cannot exhaust the burial's. It removes the regression below — speculation could never turn a finished burial into a halt, because running out would simply leave the arm unreduced. It was rejected because the residue would then depend on the budget: how far an arm got would be a function of how much fuel was left, two budgets would give two residues, and §8.2 says a budget is not recorded in a trace precisely because it cannot have affected one. Buying safety with a trace that depends on the invocation is the wrong trade twice over.

A keyword that asks for it. opaque makes burial do less and nothing makes it do more, so the symmetric answer is a second keyword and speculation only where it is written. Rejected on size. It is a keyword to buy back behaviour that is correct by default, and this language already spends one of its eleven rules on the other direction.

What was taken instead is speculation with three things forbidden: a speculative reduction may not form a hole, may not deposit, and may not collapse. The first two are §6.2's reason turned into a rule. The third is subtler and is the one that would have been got wrong: an out-of-range slice in an arm the world never takes would otherwise cave in the burial, which makes whether a program buries depend on how far a specialiser got — the same objection that killed rescue earlier in this section, arriving from the other side.

What it cost. A program that buries today may stop burying, because an arm that never terminates is now reduced until the budget runs out. It is a smaller loss than it reads as: such a program only buried because the world answered the way that avoided the arm, and had it answered the other way the burial would not have finished either. Speculation turns a conditional non-termination into a certain one. opaque is the control for the case where it was meant.

Also paid: both arms are reduced and one is thrown away, so the work is charged for a path that may not exist and the residue carries both. That is the ordinary price of a polyvariant specialiser and it is why opaque is in §6.4 rather than here.

Stopping a block at the first statement that starved

§6.5 used to stop a block at the first statement that starved and leave every statement after it unreduced, even after undecided branches began reducing their arms in place.

Leave it stopped. On contact with lib/interpreter.nc, that rule undid branch speculation completely. An interpreter binds the result of evaluating a sub-expression before branching on it (Bytes r = expression(...); if (failed(found(r))) ...), so the statement before the branch starves first and the branch is never reached. Stopping at the binding meant the bootstrap residue was unchanged to the byte.

Reduce what follows without speculation, or reorder pure statements ahead of the starved one. The statements after a starved binding are not undecided in the way an if arm is — if the starved statement finishes, the next statement runs — so it is tempting to evaluate them ordinarily. Rejected because the starved statement has not happened yet: a deposit after it that was recorded now would appear in the trace before whatever the starved statement deposits when the world answers, and a return after it that left the block now would discard the starved statement and the hole inside it. And a statement after an if that branches on the starved binding may never be reached at all if the branch returns, so a collapse or a hole there has the same standing as one inside an undecided arm.

So the statements and tail after a starved one are reduced in place under the same three clauses as an undecided arm, with the starved binding held as an unknown local and statement order preserved.

What it cost. A statement that collapses or jumps out of a loop after a starved one has its speculative work rolled back and leaves the remainder of the block unreduced.

Depth as a monad stack

The obvious alternative to a lattice. Rejected because effects that compose by max need no lifting, no transformers, and no ordering decisions, and because max is a rule every programmer already holds in their head.

The cost is expressiveness: a lattice cannot distinguish reads the disk from reads the disk and the network except by taking the deeper of the two. Nether C accepts a coarser answer in exchange for one people will actually use.

Monotonicity, pointing the other way

§2.4 once required d′ ≥ d and explained it as evaluation can only ever learn that something is deeper than it looked. It reads well and no implementation can satisfy it. A conditional's depth is the maximum over its arms, and reducing it takes one arm and discards the other, so a branch whose deep arm is not taken reduces to something shallower than its own type says. The generative test in 0052 found it in forty-seven programs.

Keep ≥ and make the arms not count. Give a conditional the depth of its condition only, so reduction never lowers anything. Rejected outright: the arm that is taken carries its own depth into the result, and a rule that drops it hands back a disk-derived value typed as pure. That is laundering, and it is the one thing the lattice is for.

Keep ≥ and make reduction preserve the bound. Have burial stamp the unreduced expression's depth onto whatever the branch reduces to, so 1 becomes 1@3. The law holds and the language stops working: pure code that happens to sit beside a deep arm no longer disappears at burial, and everything downstream of it inherits a depth nothing ever reached.

What it cost. The shorter, more quotable sentence. d′ ≤ d is the direction that carries the guarantee — a value never escapes at a depth its type did not admit — and it costs the intuition that a depth is something already reached. It is a bound, and the number that was reached lives in the trace, which is now said explicitly in §2.4 because the two were being read as one.

Pretending an implementation has no limits

§6.4 said exhausting fuel was a diagnostic and not a crash, and left it there. Fuel bounds steps, so a recursion that never returns overflows whatever stack the implementation is using long before the budget runs out, and a stack overflow is a crash. The guarantee was true of the case it named and silent about the case that actually happens.

Bound depth with fuel. Charge more of the budget per frame, so that a deep program exhausts sooner. Rejected because it changes a constant and not a shape: for any per-frame charge there is a budget large enough to reach any depth, and picking one small enough to be safe makes fuel useless as a bound on work.

Say nothing and let implementations differ. Rejected because §6.4 already promises no crash, so saying nothing is not neutral — it is a promise no recursive evaluator can keep.

What it cost. An admission: two implementations with different limits can disagree about whether a program buries at all. The reproducibility claims in this document survive because none of them was ever about that. They are about what a trace is once it exists, and the sentence that says so is now written down beside the admission rather than assumed.

One number on an arrow

An arrow carried a single depth, and [ABS] took it from the body's value depth. The consequence was that a descent could be written and not named:

nether c

Bytes load(Str p) { descend disk { must(read(p)) } }

Bytes src = load("kernel.nc");   // rejected: dƒ was 3, δ was 0

while §1.3 opens by accepting the identical expression written out at the same ambient depth. There was no way to put a descent behind a name, and the same rule failed in the other direction too: a function whose deep work was deposited rather than returned had a body of value depth 0, and so claimed a latent depth of 0 while touching the disk.

The decisive objection is about burial rather than taste. Burial reduces applications, so under that rule an application could be rejected where its own inlining was accepted, and the residue of a burial is supposed to be a program that checks. Two ways to keep the single number were considered.

Let the latent depth be what the body reaches, and let a descent inside a body not relieve the caller. A signature then reads as an audit: U0 stamp() @4 says it writes to the disk, and that is worth something. But a descend inside a function bounds nothing under this rule, so every caller up the chain holds what the leaf reached, and a program that reads one file writes descend disk at every level between the two. Encapsulating a capability becomes impossible, which is most of what a capability is for.

Carry three numbers — what it asks of the caller, what it hands back, and what it reaches — the third purely so a signature stays an audit. Rejected because the audit answer is already recorded somewhere better: a trace lists every stratum actually reached, with a witness for each, and nether strata reads it. A number in a signature that no rule consumes is a comment with a syntax.

What it cost. The chosen design has two numbers and a signature is no longer a complete account of what a function touches: U0 stamp() can write to the disk and say nothing about it in its type, because it descends for itself and hands back U0. What a program did is a question for the trace, and what a program needs from you is the question the type answers. That split is defensible and it is still a real loss for anyone reading signatures to decide whether to call something.

[APP]: the premise on all three terms

[APP] once required max(dƒ, d_f, d_a) ≤ δ, which reads well — everything about this application is within what you hold — and forbids §6.2's own example, where compile(src) is applied to a depth-3 value at ambient 0 and the comment beside it says the call is pure and merely starves. §9.2 does the same with given(a), and §2.5 says in prose that a shallow value combines with a deep one without coercion.

The stricter premise is not unsound; it is unusable. Under it a value carried out of a descent can be sealed, shaded and compared, and cannot be passed to len, so every use of a deep value has to happen inside the descent that produced it and staging buys nothing. That is close to deleting §1.3's one-way-out property.

What replaced it is the narrowest premise that still stops the thing capabilities exist to stop: the latent term, and only that one. A capability is required to reach a stratum, and dƒ is the only term that reaches one. It was written dƒ ≤ δ until δ became a set; it is dƒ ⊆ δ now, and the entry below is why.

Ambient soundness: two ways to keep the simpler statement

§2.4 once said d ≤ δ outright, which is shorter, easier to check and false: [DESCEND] carries a value out at the depth it reached, and Bytes@3 src = descend disk { read("kernel.nc") }; is depth 3 where δ is 0. Two ways to keep the shorter sentence were considered.

Let a descent forget. Conclude descend κ {e} : τ@δ instead of τ@d. The invariant then holds by construction, and so does nothing else: it lowers the depth of a value, which §1.2 forbids outright, and it turns the one expression in the language whose purpose is to reach the world into the one expression that launders what it found.

Let a descent stain. Keep δ raised for the remainder of the enclosing scope, so that anything holding a depth-3 value really is at ambient 3. The invariant holds, and the cost is that a capability's extent is no longer visible in the braces: a descend disk on line 4 silently grants the disk to line 90. This is the same re-staining already rejected for look earlier in this section, and it is no better here.

What was kept instead is a longer true statement. The cost is that ambient soundness now has a term in it that a reader has to evaluate — g(e), the deepest descent in the expression — where before it had two symbols. A rule that fits on one page is worth defending; a rule that fits on one page and is wrong is not.

One range for all three integer spellings

Every integer literal could hold the same range, which is easier to state and leaves −2⁶³ unwritable: - is an operator applied to a literal, so the literal it needs is 9223372036854775808, which is one past the top of the range. C has this wart and works around it with implementation-defined promotion; a language with one integer type and no promotion has nowhere to put the workaround.

The alternative considered was to let a decimal literal reach 2⁶³ — one higher than the type — on the grounds that it is only ever going to be read under a minus sign. Rejected because it makes a bare 9223372036854775808 a literal that is in range as a literal and out of range as a value, which is a distinction nothing else in the language makes and which every reader would have to be told about once.

What it cost. Three spellings with two ranges between them, and a sentence in §3.6 explaining why. The alternative is one range and a value that cannot be written, and a type with a value nobody can write is a type with a hole in it.

A declared set the trace does not hold

§9.4 used to say a trace records the declared set as well as the values read from it. §7.3.1 is frozen and a Trace has no field for one, so the sentence described an implementation that could not be written.

The alternative considered was to unfreeze the node encoding and give Trace a seventh member: the cairn of a canonical list of declared names. Rejected on what it buys. A name that was read is already a Witness — including one declared and unset, because §9.9 makes a refusal an answer and an answer is witnessed. A name that was never declared collapses and there is no trace to put anything in. So the only thing the field would record is a name that was declared and never read, and the only thing it would do is make two traces differ over something that changed neither of them. Content addressing is the claim that two identical programs have one name; a field that breaks that to describe the invocation is a field that makes the ledger worse.

What it cost. The invocation is not recoverable from the trace. Somebody holding a sealed trace can see every environment variable the program read and cannot see the ones it was offered and ignored, and no rite will tell them. That is the price of the cairn meaning what it says.

A cairn with no way to write it

§3.6 had no cairn literal, on the reasoning that a program never needs to write one: a cairn is something seal produces, and sealing is how you get one. That is true of a program somebody writes and false of a residue, and §6.5 makes a residue a program. Cairn c = seal b"hi"; demand c; buried to a residue whose second line read demand «a cairn has no syntax»;, which does not parse.

The alternative considered was sixty-four hex digits with no mark in front. Rejected because an identifier may begin with a letter and deadbeef is both a plausible cairn prefix and a plausible variable name; a lexer that has to count to sixty-four before it knows which token it is reading is a lexer whose error messages cannot be written.

Also rejected: allowing the short form the rites accept. nether lamp 76c4b655 works because a ledger is there to resolve the prefix. A program is read without one, and a literal that names one thing on this machine and two on the next is not a literal.

What it cost. A sixty-five character token, and the # that C programmers will read as a preprocessor directive for as long as anyone remembers what one was.

Deposits in source order

§8.4 used to render deposits grouped by the cairn of the source they came from, ordered by offset within each group, on the reasoning that a trace's sources were never written down in a sequence. They were: a sealed trace's deposit list is the order the deposits were made in, and the sort threw it away. Its key began with thirty-two bytes of hash, so which half of a program's output came first was decided by a digest, and a comment added to the top of a file reordered what lamp printed.

Ordering by offset within one source looked like the safe half and was the same mistake one level down. A function called from two places deposits in call order from one span, and offset cannot tell those apart.

What it cost. Nothing that was true. A reader who wanted the deposits of one source together, in the order the text has them, now has to ask for that rather than getting it by default — and nothing asks, because a program's output is read in the order it was made.

Grafting an answer that was already given

§8.7 used to accept an answer the trace had already been given as a thing to replace. It counted it, reported 1 recomputed, and returned a trace naming the substitute witness beside the deposits the original answer produced, because a sealed trace's residue no longer holds the work that consumed the answer and re-burying it produces nothing.

The alternative considered was to make it work: re-bury from the trace that still had the hole, which is the only thing that can produce the right deposits. Rejected because a sealed trace does not name the trace it was exhumed from — nothing in §7.3.1 points backwards — so graft would have to search the ledger for a parent, and a ledger may hold several or none. Re-burying the source from scratch instead would reach a trace with a different residue and a different name from the one exhuming the parent would have reached, which is two names for one result.

What it cost. A person holding only the sealed trace cannot ask "what if this file had said something else" of it. They need the trace from before it was answered, which they had, because they exhumed it.

A trace's depth without its holes

§7.3.2 used to make a trace's depth the join of its residue and its witnesses. A hole contributed nothing, on the reasoning that the residue already counts whatever the holes would reach. §1.5 makes that false: seal e is depth 0 whatever e is, so a program that demands a fetch only through a seal buried to depth 0 with a stratum-5 hole under it, and strata printed pure over a trace that could not take a step without the network.

The alternative considered was to leave the formula and make the residue carry the depth of what it seals. Rejected because it unsays §1.5: a seal is pure because naming a value does not touch the world, and a residue that counted sealed expressions would make every program that keeps a cairn as deep as the thing the cairn names. Counting holes instead of the residue was rejected already, by opaque, which hides a deep expression that never becomes a hole. Counting them as well is the only rule both cases agree with.

What it cost. A trace's depth is no longer a fact about its residue alone, so bury reads every hole it is about to write back out of the ledger, and a trace written before this rule may now be malformed by §8.6 without anything about it having changed.

A refusal that knows its own type

§9.2 gives a program answered and refused. refused(absent) carries no T, and the IR's types have no variables, so it takes T from the binding or return it is the whole value of and is an error anywhere else.

Three alternatives were considered.

No constructors. Leave every Answer to the prelude. Rejected because it made utf8 a pure function that does what no pure program function can, and a program that parses had two ways to say no: collapse, which forbids its caller from handling anything, or return a Bool beside a value, which is the shape Answer exists to replace.

Type variables in the IR. Leave refused's T unknown and solve for it. Rejected on what it costs: inference is a second type system beside the depth calculus, which is eleven rules on purpose, to type one function whose T is written down a few characters to its left in every program anybody would write.

A type argument. refused<Bytes>(absent). Rejected because it is new syntax for one call, and it says again what the declaration already says.

answered alone, without refused, was not considered seriously: a program that can say yes and not no is worse than one that can say neither.

What it cost. refused cannot be an argument. given(refused(absent)), first(refused(absent)) and a refused written as a function's tail value with no return are all errors, where a language with inference would accept them. Each has a one-line rewrite through a declaration, and the error says which. And refused sits one letter from refusal, which is the inspector pointing the other way; the types differ, so the typo is caught rather than believed.

Parenthesising every expression a residue prints

print, which writes a residue back out as source (§6.5), used to wrap every operator in parentheses. The reasoning was that the round trip is about meaning, and a printer that leaned on §4.6's table to rebuild the shape would prove the table rather than lowering. It also added a level of nesting the source never had for every operator it printed, and §6.4's limit on nesting reads the printed form like any other. A flat sum of 80 terms buried, and its residue came back 79 parentheses deep and could never be exhumed.

The alternative considered was to keep the principle and stop the damage: print a left-nested chain of one operator as one parenthesised run. Rejected because it is the precedence table again, used for associativity only, and it fixes the chain while leaving every other way an expression can be long.

The printer now parenthesises a child only when its level is looser than its place allows, and reads the levels from the table the parser climbs. Minimal parentheses never nest deeper than the source that lowered, so what lowers prints as something that lowers, and the fuzzer holds that over every input.

What it cost. The round trip now depends on the printer and the parser agreeing about §4.6. They read one table, so they cannot disagree by drifting, but a wrong table is now wrong in both places at once, and the round trip cannot see it. §4.6's own proof, which compares the table with §04, is what catches that.

Burial that holds the store

§8.2.1 lets bury remember a burial it already did. The first proposal was for burial itself to consult the store before evaluating, which makes burial hold stratum 1, which makes bury grant store by default. Rejected because it unsays §8.2: with no --grant, burial holds no capability, and that is the default precisely because it cannot surprise anyone. A burial that can read the store can read a node somebody else wrote, and then two stores give one source two traces.

The memo is the rite's, not the program's, and holds nothing the store does not.

Also rejected: reporting zero steps for a remembered burial. Steps are a fact about the burial, and §6.4 asks implementations to agree on them. An implementation that remembered would report a number one that did not could never reproduce, and the budget would mean something different on each. So the rite reports the steps the burial costs, says it remembered, and refuses the memo when the budget would not have covered them.

What it cost. A memo entry records the steps a burial spent, outside the trace, and that is a second place the number lives. It is never read except to compare with a budget, and an entry that disagrees with the trace it names is the same as no entry: the rite buries.

A newer release that replays older traces

§0.6.1 promises that an old trace can be replayed by the release that wrote it, not by every release after. The alternative considered was the stronger promise: each release carries what it needs to bury the residues of the ones before it, as a compatibility mode keyed on the trace.

Rejected on cost and on honesty. Every semantic change would leave a branch behind in the evaluator for as long as old traces exist, which in a ledger without garbage collection (§7.6) is forever. And a compatibility mode is a second implementation of the old release written by people who have since changed their minds about it, which is a worse witness to what the old release did than the old release itself. Reproducible builds make the old release recoverable, and recovering it is the honest way to ask what it would have done.

What it cost. Replaying a trace from two majors ago means fetching and running a two-majors-old binary. Somebody who only has the newest release cannot do it.

A parallel burial with an order of its own

§6.2.1 requires a parallel burial to leave the trace the serial order would. The alternative considered was to let each implementation order holes and deposits however its threads finished and to compare traces as sets.

Rejected because the order is not decoration. A hole list is read in order by exhume and by every person reading strata, a deposit list is a program's output in the order it was made, and which of two places asked a shared question first is the span the hole keeps. Comparing as sets would let two burials of one program disagree about all three and still be called the same, and the trace's cairn — which is built from those lists in order — would differ between them anyway.

What it cost. A parallel burial has to keep enough of the serial order to commit results in it, which is bookkeeping a free order would not need, and a collapse found early on another thread has to wait to be reported.

Answering every hole in a trace at once

§6.6 lets an exhumation overlap a contiguous run of read-stratum holes and keeps act-stratum holes sequential. Two broader rules were considered.

Overlap every hole in the trace, since §6.3 guarantees finished arguments. Rejected because finished arguments mean no hole waits on another hole's value; they do not mean the world is indifferent to the order in which it is touched. A read asked concurrently with a write to the same path sees one of two files depending on which thread won, and two posts in flight at once arrive in network order rather than demand order.

Record witnesses in completion order. Rejected for the same reason §6.2.1 rejected completion order for holes: the witnesses list is part of the Trace node, so its order is in the cairn, and §6.3 serves multiple answers to one call in list order.

What it cost. A write between two reads splits the exhumation into two sequential read batches around the write, even when the paths are disjoint, and a fast hole after a slow one waits to be committed in discovery order.

Walking the reverse index to find damaged traces

§7.5.2 derives affected traces by walking forward from verified Trace nodes rather than walking refs/ backwards from corrupt objects.

The alternative considered was to start at each corrupt object and follow referrers up to every Trace that names it. Rejected because an audit has to inspect objects/ anyway to find the corrupt objects, and refs/ is the very derived index the audit is checking: a missing reverse edge would make a damaged trace look healthy, and a corrupt object that was itself a Hole, Witness or Deposit has outgoing edges that cannot be decoded at all.

What it cost. An audit decodes every verified node in the store to read its forward references, even when only one object is corrupt.

Reconciling stores by whole-inventory diff or by shipping `refs/`

§7.5.3 reconciles two stores top-down from explicit root cairns $R$ in bounded want batches and exchanges only canonical objects. Three alternatives were rejected.

Whole-store inventory exchange — trading a full list of stored cairns, a Bloom filter, or a prefix trie over the whole store so the difference can be computed in one pass. Rejected because a store never shrinks (§7.6) and holds every unrelated burial that machine has ever run. An inventory exchange scales with the size of both stores rather than the size of the trace being asked for, and hands a stranger the names of every private trace in the store.

Shipping refs/ or memo/ alongside objects/. Rejected because both are derived indexes: a receiver that trusted a peer's refs/ would accept forged provenance edges without the peer having to forge a blake3 hash, and memo/ is keyed by a single machine's executable (§8.2.1).

Treating divergent witnesses for one call as a conflict. Rejected because a Witness node records what the world answered at one exhumation, not a mutable slot for "the current answer". Two exhumations that received different answers have different witness cairns and different trace cairns, and a store that holds both has lost nothing and contradicted nothing.

What it cost. Top-down reconciliation takes one round trip per level of the root's node graph instead of one round trip for the whole store, and the receiver decodes each object and rebuilds its own refs/ entries on arrival.

Moving a store by copying its directory

§7.5.4 exports a store as a dependency-ordered stream of verified objects with a whole-stream blake3 trailer and rebuilds refs/ on import.

The alternative was to document tar (or a directory copy) followed by an audit at the destination. Rejected because a directory copy transfers refs/, memo/ and leftover files in tmp/, trusts the source filesystem not to have corrupted an object silently before the copy, and leaves a truncated transfer with nodes in objects/ whose referenced children have not arrived yet.

What it cost. Exporting reads, decodes and hashes every object in the source store to order and frame the bundle, and importing decodes, hashes and indexes every object again at the destination.

Assigning distributed holes by `Call` or resolving conflicting witnesses by arrival

§6.6 assigns a trace's open questions across machines by their slot index 0..holes.len(), commits merged witnesses in ascending slot order, and rejects conflicting witnesses for the same slot. Two alternatives were rejected.

Assigning and merging by Call or by Hole cairn. Rejected because at act strata (4, 6, 7 and 8) two entries in holes are not merged (§6.3): they may share the same Call, and when written at one source span they share the same Hole cairn (§7.3.1). Keying a delivery by Call or by Hole cairn cannot tell whether two witnesses from two workers are answers to two distinct act slots or two competing answers to one slot.

Resolving conflicting witnesses by arrival order, worker rank or quorum. Rejected because at the store level two divergent witnesses are both valid historical records (§7.5.3), while a single trace can record only one witness per answered hole slot. Picking one silently discards a recorded observation of the world and makes the merged cairn depend on which worker answered first.

What it costs. Every worker delivery carries explicit slot indices against a specific base trace T, and a retried or overlapping assignment whose world changed between attempts fails the merge with an explicit conflict rather than producing a trace.

Version ranges, a central package registry, and a dedicated ledger tag for packages

§7.5.5 represents a package as a canonical Struct value ("Package" / "Dep") addressed by its cairn, pairs local aliases with exact dependency cairns, and resolves dependency closures offline. Three alternatives were rejected.

Version ranges and a solver. Rejected because a version range resolves to different bytes depending on when and against which index the solver runs. Two disconnected machines can only resolve a dependency to the same cairn offline if the dependency names the cairn directly.

A central registry for human names. Rejected because a global namespace reintroduces a mutable mapping from names to bytes outside the ledger. Scoping an alias to the "Package" struct that declares it gives humans a readable local name while keeping every cross-package edge an immutable 32-byte cairn.

A new value tag or node kind for packages. Rejected because a package is a record of existing ledger primitives (Str, Cairn, Array, Struct), and encoding it as an ordinary Struct under tag 0x10 requires no change to the frozen tag table (§7.1) or domain separator (§7.2).

What it costs. Updating a deep dependency changes its cairn and therefore the cairn of every package above it in the DAG, and offline resolution requires the dependency closure to be imported into the local store beforehand (§7.5.3, §7.5.4).

A stateful language server for editor hover and provenance

§8.4.1 serves editor hover, depth blame and provenance through a stateless nether lamp <cairn> --at <byte> [--source <path>] invocation backed by the trace already in the ledger, paired with a thin editor adapter (tools/vim/nether.vim).

The alternative was a long-running Language Server Protocol (LSP) daemon that maintains an in-memory workspace and re-checks unsaved buffers on every edit. Rejected because provenance, holes, witnesses and deposits only exist for a program that has been buried into a trace: an unsaved buffer that differs from trace.source has no recorded nodes at its edited byte offsets, and walking provenance on an unburied buffer either serves shifted spans from an older trace or silently buries on every cursor movement. Refusing when --source <path> disagrees with trace.source states the boundary between unburied text and a recorded burial.

What it costs. After editing a buffer, a programmer must run nether bury again before lamp --at will inspect the new trace, and the adapter covers hover depth, descend origin navigation and recorded-node provenance rather than general LSP features such as completions or rename.

`https`, and the one dependency exception

CLAUDE.md permits exactly one kind of dependency — "do not write your own cryptography" — and refuses the rest. https is TLS, so §9.6 had to settle whether net means a TLS stack or means less than people will expect.

It settles neither, deliberately: the scheme set is the implementation's, and what §9.6 requires is that it be stated and that a scheme this build will not serve come back denied rather than unreachable. This implementation serves http and refuses https by name.

The alternative considered was a TLS dependency — rustls and a root store — on the grounds that a net capability that cannot reach most of the network is a capability nobody will grant. Rejected for now on what the stratum is for. The interesting content of strata 5 and 6 is the witness and the replay: a response sealed on arrival, served back from the ledger, with no socket opened. None of that is about TLS, and all of it can be demonstrated without it.

What it cost. nether exhume --grant net will not fetch from most of the web today, and anybody who needs it to has to build with a TLS stack this repository does not ship. That is a real exclusion and it is stated here rather than discovered.

The network's reach

§8.3.2 makes --grant net insufficient on its own: a host has to be named as well.

The alternative considered was the capability alone, on §9.1's reasoning — a capability is the audit point, and the whole apparatus exists so that a reader can see what a burial may touch by reading one line of the invocation. Rejected because it makes net the one capability with no bound on what. An implementation already roots the disk somewhere, for a reason it states in its own source: a burial able to read /etc/shadow because a program asked it to is a burial nobody can grant a capability to. A socket is that argument with a longer reach.

What it cost. A second flag, and an invocation that fails when somebody grants net and forgets --reach. The failure is the cheap one — the trace is not written, rather than written against a host nobody meant to allow.

Who frees what, across the foreign boundary

§9.8.1 makes the caller own both buffers and calls twice when the first is too small.

The alternative considered was the usual one: the callee allocates its answer and the caller frees it. Rejected because it makes the two sides share an allocator, which they do not — a Rust caller and a C callee linked against a different libc free from different heaps, and the failure is a corrupted heap at some later, unrelated moment. A protocol whose failure mode is "something else crashes an hour from now" is a bad protocol in any language and an unusable one in a language whose whole argument is that you can tell what happened afterwards.

What it cost. A callee that cannot size its answer in advance is called twice, and does its work twice or caches it itself.

A foreign call, and the one `unsafe`

The workspace sets unsafe_code = "forbid". A foreign call cannot be written under it, so §9.8 needs somewhere for the exception to live.

The alternative considered was relaxing the lint where it was needed — an allow on the module that does the call. Rejected because forbid exists precisely so that it cannot be locally undone, and downgrading it to deny to make one module possible makes every other module possible too.

So the exception is a crate, and nothing else in the workspace changes. §1.7 says this stratum is quarantined loudly; this is the same quarantine one layer down.

The rule that came out of it is narrower than "unsafe is allowed here": unsafe lives only where the language ends. There are two ends — the one where Nether C calls out, and the one where something else calls in — and each is a crate whose Cargo.toml says so.

What it cost. A crate boundary where a module would have done, and two Cargo.toml files that say unsafe_code = "allow" in exactly the places a reader will go looking for them.

A bound on reading, and why it is not ten

0219 set out to show that no input under a megabyte costs more than ten megabytes. Rejected, because no tree can meet it: a ; is a token and a statement, and a 0x00 inside an array is a 48-byte value, so one byte of either input is several dozen bytes of what it means. Meeting ten would mean not building the tree.

What was kept is the half of the claim that was about attack: what a reader allocates is linear in what it was given, with the multiple stated and asserted (SECURITY.md, boundaries 1 and 2). Measuring it found the case the claim was written against — an array nested in arrays, each believing a count against the same remaining bytes, reserved five gigabytes from one megabyte — and it was in the codec, which had been looked at twice.

What it costs. A megabyte of source can hold a quarter of a gigabyte while it is parsed. That is a large constant, and it is a constant: it cannot be bought with a cleverer megabyte.

Floating point

Excluded from §3.6 because IEEE 754 has platform-observable behaviour, and canonical encoding cannot be built on top of it. This makes Nether C unsuitable for numerical work today, which is a real and large exclusion.

90.3 Things Nether C is worse at

Stated plainly, because the roadmap requires at least one such statement and because they are all true.

Interactive programs. A language whose central act happens before the program is delivered is the worst possible fit for anything that responds to a person. Nether C should not be used for a UI, a game, or a server that holds a connection.
Numerics. No floats. See above.
Debugging by print. Two commands instead of one, forever.
Storage. The ledger never shrinks. §7.6 argues that this is affordable; it has not yet been measured, and until it is that argument is a hope.
Keeping a secret. Depth is a claim about where a value has been, not about what it can be made to reveal, and the two get confused because a lattice is what a confidentiality type system looks like too. §1.5's seal is the shortest demonstration: the cairn of a depth-3 file is at depth 0, hex makes it text, and equality on it decides something about the file while holding nothing. A program that must not reveal a deep value cannot be checked by this type system, and nothing in the language is going to make it one.
Writing a container. A program cannot abstract over a type. func_decl (§4.2) has no type parameters, §3.8 removed the preprocessor and §5.2 removed pointers, so there is no macro, no void * and no generic to fall back on. The prelude's own signatures are generic in T — must, given, answered — and nothing a program writes can be. A C programmer reaches for a container on day two and this language has no way to write one: the answer is one type per element type, by hand, and that is the whole of it in this draft.
Learning curve. Depth is a genuinely new thing to learn. HolyC's whole proposition was that you already knew it — it was C, plus permission.

90.4 On TempleOS

Nether C is an inversion of HolyC in the way a photographic negative is an inversion: every value reversed, every edge in exactly the same place.

Terry Davis built a complete operating system, a compiler, a graphics stack, a document format and a language, alone, and made every one of them follow from a single stated idea. Whatever one makes of the idea, the coherence is the achievement, and it is rarer than the code.

He was ill, and it is in the work. TempleOS is strange because he was strange, and it is also technically excellent, and both of those are true at once and neither one cancels the other. Treating the strangeness as the whole story misses an operating system. Treating it as an embarrassment to be edited out misses the person who wrote it. This document tries to do neither.

What is borrowed here is the method rather than the belief: build the thing yourself, keep it small enough to hold in your head, follow one idea all the way down even when it becomes inconvenient, and say plainly what you think is true.

An inversion is a form of close reading. You cannot turn something over without first working out which way up it was.

90.5 Two rooms, one colour vocabulary

The interface uses indigo grounds and rose signals. Its light companion uses rose porcelain, lavender panels and plum ink. Both are authored in site/design.py; generated CSS, GIF colour tables and the cairn icon consume those roles. The nine depth colours follow a violet-to-rose path, but numbers and labels remain the authoritative cues.

Rejected: complementing the RGB values or applying a filter to the page. Neither preserves readable contrast or gives the light room a character of its own. The old VGA swatches also described colours the interface no longer used; swatches now show live semantic tokens.

What it costs. Two small colour tables and a second set of GIF files. The drawings, timing and encoders remain shared. Tests compare both shipped colour tables against the system and check text on plain and raised surfaces. The hero and descent have still counterparts for reduced-motion readers.

90.6 One face, and where the lettering is not type

Everything on the page that is text is Nether 8, the one 8×8 face site/font.py draws — the prose, the headings, the listings, the sign and the lamp. The headings are not a second face. They are the same letterforms at 24px and 16px against a body at 16px, and what makes a heading look like one is around the letters rather than in them: colour, uppercase and letter-spacing on h1, a filled bar on h2, and the ██, ■ and ▸ that precede the three of them.

That reads as deliberate. It is, and this is where it was decided rather than left.

The repository does hold a second alphabet, and it is not a counter-example. site/gfx.py has a 5×7 one of fifty-one characters — capitals, digits and a little punctuation — and it is drawn into GIF frames pixel by pixel at whatever scale the picture needs. It is lettering inside a drawing. It cannot be selected, searched, or read aloud, it has no lowercase, and nothing on the page sets text in it. Two alphabets, one of which is type and one of which is not.

Rejected: a display face for the headings, drawn on a bigger grid. It is the obvious other answer and it costs three things. A second set of a hundred and thirty-eight glyphs, which is the smallest of them. A second .woff for a few dozen words per page. And a second grid — the face is a pixel face on an eight-unit cell and the type scale is 8, 16, 24, 32, whole multiples of it, so every pixel of a glyph lands on whole pixels of the screen. A display face drawn on twelve or on sixteen either brings a scale that is not a multiple of the body's, or is the body face larger, which is what is already there.

The idiom settles the rest of it. These headings are DOS window title bars. A poster face would make them posters, and the front page would stop agreeing with the terminal it is describing.

What it costs. A heading carries no information in its letterforms that a paragraph does not, so all of the hierarchy is in colour, case, spacing and three block characters. A reader who cannot distinguish --accent from --ink has the prefix and the bar, and that is the whole of it. It is thinner than a display face would be and it is the price of one face.

A second weight is a different question, and it is item 0231: bold is the same letterforms drawn heavier, not a second face, and the browser must not be allowed to invent one.

The four sizes it is read at, and where the grid gives way

Nether 8 is drawn on an 8×8 grid with a seven-unit fixed advance (six ink columns and one blank bearing column). site/design.py emits four sizes and no others (TYPE = {8, 16, 24, 32}), whole multiples of the drawing cell:

8px (--type-fine, 1× cell, 7px advance): the ASCII door sign (pre.sign, line-height: 1 = 8px), listing captions (figcaption), plaque title bars (.plaque > h3), the footer, badges, the hit counter, and the 8×8 drawing grids and metadata on site/specimen.html (line-height: 1.375 = 11px).
16px (--type-body, 2× cell, 14px advance): body prose, code listings (pre, code), tables, navigation and directory drawers, terminal status bars, controls (button, textarea), necropolis labels and previews, and h3/h4 (line-height: 1.375 = 22px; textarea uses 1.5 = 24px). html sets font-size: 14px solely to scale rem margins and padding; body restores 16px before any text is drawn, and @media (max-width: 640px) tightens padding without lowering the body size.
24px (--type-head, 3× cell, 21px advance): h1, h2, .necropolis h2, and .box.covenant strong (line-height: 1.375 = 33px).
32px (--type-sign, 4× cell, 28px advance): .necropolis h1 (line-height: 1.25 = 40px) and .nc-selected h2 (line-height: 1.375 = 44px), plus the 4× specimen row and glyph samples on site/specimen.html.

Every line-height (1, 1.25, 1.375, 1.5) and every letter-spacing (.125em) in site/nether.css is a multiple of one eighth (1/8), and because every allowed font-size is a multiple of 8px, their products are always whole CSS pixels (8/11/16/22/24/32/33/40/44px leading; 1/2/3/4px tracking, bringing a tracked character's pitch from 7/8 em to 1em). An earlier .necropolis h1 rule at 48px with line-height: 1.2 (57.6px on desktop, 38.4px on mobile) and decimal tracking (.1em, .12em, .08em, .06em, which shifted characters by 0.64px–2.4px) were brought onto the eighth grid in 0234, and tests/css/run and tests/necropolis/browser.mjs refuse any element whose computed font-size, line-height, or letter-spacing leaves it.

Rejected: scaling body or code down to 12px or 14px on mobile, or using 8px for running text. At 12px or 14px (1.5× or 1.75× the grid) every second stem straddles a device pixel at scale 1; at 8px (1×) a bold stem is two pixels and a counter in B, 8, 0, a, e, or g is one pixel wide, which holds for short uppercase chrome and captions and is too tight for a paragraph or a code listing. Also rejected: retiring 8px from chrome and captions altogether, which would double the height of the door sign and make listing title bars as tall as the code they label.

What it costs. Three things CSS integer pixels cannot prevent:

At 8px and device scale 1, one drawing unit is one physical pixel. Closed counters remain open across both weights, but dense forms (@, %, #, §, m) have single-pixel gaps that only gain breathing room at device scale 2 (2×2 physical pixels per unit) or at 16px and above.
Outline rasterisation on scanlines beside crossbars. Nether 8 ships as quadratic contours in glyf rather than embedded bitmap strikes (EBDT), so Chromium and CoreText still apply greyscale coverage antialiasing on rows immediately adjacent to horizontal bars even when -webkit-font-smoothing: none is set.
Non-integer browser and display zoom. At 125% (1.25×) only 32px (40 physical pixels, 5× the grid) lands on whole physical pixels; 8px, 16px, and 24px become 1.25×, 2.5×, and 3.75× the grid, giving the two stems of H asymmetric physical widths (1.62 vs 1.82 pixels at 8px). At 150% (1.5×) the even CSS sizes (16px and 32px) land on whole physical pixels (3× and 6× the grid) while the odd sizes (8px and 24px) fall on halves (1.5× and 4.5×). Integer CSS pixels keep 1× and 2× screens exact and keep 16px body text exact at 150%, and cannot make every zoom factor an integer multiple of eight.

Mechanizing the metatheory: an in-tree LCF proof kernel versus an external proof assistant

§2.4 states two properties an implementation must preserve — soundness of the bound (reduction never raises depth) and ambient soundness (any derivable depth is bounded by max(δ ∪ g(e))) — and §1.6, §6.8 and §7.1 add three more: the necessity and sufficiency of the Orpheus premise d ∈ δ, the staging law bury(bury(e, A), B) = bury(e, A ∪ B), and the injectivity of the canonical encoding. Generative testing (0052) checks ten million random derivations and reduction steps, which is a strong regression net and not a proof.

Four families of proof environment were compared for proof/:

External interactive proof assistants (Lean 4, Coq/Rocq, Agda, Isabelle/HOL). Foundational kernels with rich tactic languages and editor integration. Rejected: each brings a multi-hundred-megabyte toolchain outside the pinned CI image (.github/workflows/ci.yml pins Rust 1.98.1 and Python 3.12), version-locked standard libraries whose syntax and tactics churn across point releases, and a build step that contributors without the assistant installed would skip. A proof that only runs when an optional tool is present rots the way an optional lint does.
External SMT solvers (z3, cvc5). Fast decision procedures for quantifier-free theories. Rejected: an SMT script asserts universal axioms for inductive relations (HasType, StepTyped, encode/decode) and asks whether their negation is unsatisfiable; if an axiom set is accidentally inconsistent, unsat is reported for every theorem without constructing an inductive derivation.
Generative sampling alone (0052). Already in the tree and fast, and still finite sampling over an infinite family of terms.
An in-tree LCF-style proof kernel (proof/kernel.py) under pinned Python 3.12. Following the same rule as site/bake, site/gfx.py and site/font.py — when a small self-contained tool can be written in the tree with zero dependencies, write it in the tree — proof/kernel.py defines a sealed Theorem type gated by a private kernel token (_KERNEL_TOKEN). No code outside proof/kernel.py can construct a Theorem except through the kernel's primitive inference rules (assume, mp, imp_intro, conj_intro, conj_elim_l, conj_elim_r, disj_intro_l, disj_intro_r, disj_elim, iff_intro, inst, gen, refl, sym, trans, cong, rewrite), its inductive derivation principles (apply_rule, rule_induction, structural_induction), and its complete finite-domain decision procedure lattice_decide over Depth = {0..8} and Held = P({0..8}). proof/check.py scans every module in proof/ with Python's tokenize to reject admitted obligations (sorry, admit, admitted, axiom, unproved, postulate, todo, fixme), verifies negative kernel self-tests (forged theorems, missing induction cases, undischarged assumptions, invalid lattice formulas), and runs on every scripts/task test, scripts/task proofs and scripts/task check.

What it cost. Two things. First, the trusted computing base of the proofs is proof/kernel.py (~600 lines of Python) plus the pinned Python 3.12 interpreter rather than Lean's or Coq's kernel; proof/check.py mitigates this by testing that forged theorems, missing cases, undischarged hypotheses, and false lattice claims are actively rejected on every run. Second, proofs are written as explicit combinator and induction scripts rather than interactive tactic blocks, which is noisier for large algebraic proofs and entirely manageable for an eleven-rule calculus and an eleven-tag wire format.

90.7 What is proved, what is tested, and what is believed

A project that mechanizes part of its metatheory and tests the rest owes a reader a boundary between the two. Differential testing (0226) and generative sampling (0052) are regression checks over finite samples, not proofs; a mechanized theorem in proof/ is a proof about the mathematical model in proof/, not a proof about the Rust compiler or the host kernel.

Every claim in this specification sits in exactly one of three mutually exclusive primary tiers below. A proved claim may also carry supporting tests in crates/, and a tested claim may be motivated by a proved model theorem, and no claim is counted in more than one tier.

Tier 1 — Proved (in the `proof/` LCF model)

Reproduced by scripts/task proofs (and on every scripts/task test via python3 proof/check.py, which also token-scans proof/*.py to forbid sorry, admit, admitted, axiom, unproved, postulate, todo, and fixme, and to forbid any file but proof/kernel.py to name the kernel's seal). Each theorem below is a sealed proof.kernel.Theorem derived over the explicit inductive relations and finite-domain decision procedure in proof/:

Ambient soundness of the eleven typing rules (§2.4, theorem ambient_soundness in proof/calculus.py): for every derivation HasType(Γ, δ, e, τ, d) built from the 11 rules of §2.2, d ≤ max(δ ∪ g(e)). Model scope and assumption: proved by rule induction over TYPING_SPEC over the 9-element lattice 0..8 and capability subsets P({0..8}).
Substitution depth monotonicity (§2.4, theorem substitution_monotonicity in proof/calculus.py): for all 12 expression substitution forms SubstDepth(e, d_e, d_v, d′) representing e[x := v] with v : τ_v@d_v, d′ ≤ max(d_e, d_v), with equality to d_e whenever d_v = 0.
Soundness of the depth bound under reduction (§1.2 and §2.4, theorem soundness_of_bound in proof/calculus.py): for all 17 small-step reduction rules of §6 (StepTyped(e, e′, d, d′)), d′ ≤ d. Reduction can discard an untaken arm (if (true) a else b, where d = max(d_a, d_b) and d′ = d_a) or drop an unused deep argument, and never raises a depth.
Sufficiency, necessity, and non-interval separation of the Orpheus premise (§1.6 and §90.2, theorems look_sufficiency_ambient, look_sufficiency_confinement, look_necessity_confinement, look_necessity_numeric, numeric_vs_membership_counterexample, binding_taint_violates_ambient, and scope_restain_shifts_obligation_to_caller in proof/orpheus.py): d ∈ δ is sufficient for both §2.4 ambient soundness and {d} ⊆ δ ∪ g(s) capability confinement; necessary for capability confinement on closed shades ({d} ⊆ δ if and only if d ∈ δ); and strictly stronger than the numeric ceiling d ≤ max(δ) when δ is not a downward-closed interval (d = 3, δ = {0, 5}).
Core residual round-trip and the staging law (§6.5 and §6.8, theorems roundtrip_identity, hole_set_union_law, staging_idempotence_set, staging_law, dependent_hole_non_monotone_counterexample, and cumulative_dependent_hole_law in proof/staging.py): in the core calculus model, parse(print(r)) = r over all 11 residual constructors. The staging law is weaker than its name: StagedEval defines the two-stage reduction bury(bury(e, A), B) and the one-stage reduction bury(e, A ∪ B) rule by rule, side by side, and staging_law proves that every derivation gives both the same result. That the 17 rules of StagedEval describe what nether-bury does is believed, not proved. staging_idempotence_set is only the set identity A ∪ A = A, which turns the law into idempotence when A = B. Dependent holes whose inner capability is gated by an outer answer require the cumulative hypothesis A ⊆ B (witnessed by the non-monotone counterexample A = {0, 3}, B = {0, 5}).
Prefix-free stream round-trip and injectivity of the canonical wire model (§7.1, §7.2, and §7.3, theorems value_decode_encode, node_decode_encode, injectivity_from_left_inverse, and cairn_preimage_injectivity in proof/encoding.py): for every well-formed Value (11 tags 0x00..0x08, 0x10, 0x11, including unprefixed recursive Struct, Array, and Answer::Given) and every well-formed Node (0x20 + 6 kinds 0x00..0x05, including unprefixed Node::Literal) paired with arbitrary trailing stream bytes rest, decode_stream(encode(x) ++ rest) = (x, rest). Setting rest = b"" yields decode(encode(x)) = x, which implies encode(x) = encode(y) → x = y and injectivity of the domain-separated preimage b"netherc/cairn/v4\x00" ++ encode(x).

Tier 2 — Tested (in the Rust implementation)

These claims are about the Rust workspace (crates/), the CLI (nether), and the generated site (site/). None of them is proved by proof/; each is held by deterministic and generative test suites run by scripts/task test and scripts/task fuzz:

Correspondence between nether_core::check and a Rust transcription of the 11 rules (0226, crates/nether-core/tests/calculus.rs): model_check, a clean-room transcription of the 11 rules, and nether_core::check agree on 50,000 seeded valid and invalid Units on every cargo test (the_implementation_agrees_with_the_mechanized_model) and on 10,000,000 seeded Units across all 8 FaultKind variants in scripts/task fuzz (ten_million_programs_agree_with_the_model). model_check is Rust written from proof/calculus.py by hand. Nothing checks that the two agree, so this tests two Rust programs against each other, not the code against the proof.
Implementation burial monotonicity and residue well-typedness (0052, crates/nether-bury/tests/monotone.rs): generative testing over 10,000,000 seeded programs checking that nether_bury::bury never raises an expression's depth and always emits a residue accepted by nether_core::check.
Surface syntax print/parse/lower round-trip and staged burial on Unit IR (§4 and §6.8, crates/nether-bury/tests/residue_is_source.rs, crates/nether-syntax/tests/lowering.rs, and crates/nether-syntax/tests/fuzz.rs): surface printing, lexing, parsing, precedence parenthesisation, and two-stage burial through printed source.
Single-assignment aggregate construction and loop/branch freezing (§5.4, crates/nether-syntax/tests/frozen.rs and crates/nether-syntax/tests/aggregates.rs): checking that naming a local (seal, shade, deposit, return, argument) freezes subsequent assignments across blocks, exclusive branches, and loop back-edges while keeping loop-local declarations fresh each turn.
Production codec round-trip, truncation/trailing-byte rejection, and well-formedness guards (§7.1–§7.3, crates/nether-ledger/src/codec.rs and crates/nether-ledger/tests/fuzz.rs): cross-checking the 16 canonical fixtures against proof/encoding.py and fuzzing encode_value/decode_value and encode_node/decode_node.
Crash-safe ledger storage, multi-thread/multi-process contention, audit, exchange, and packages (§7.5 and §8, 0205–0208, 0213–0215, 0220, 0101 in crates/nether-ledger/ and crates/nether-cli/tests/rites.rs): atomic rename, corrupt-object refusal, 16-thread and 16-process contention, nether strata checking the depth a trace claims, export and import of a store, and two stores that each answer half of a trace's holes and seal byte-identically to one store that answers all of them. Every one of these runs on one machine. No test compares stores built on two architectures.
Refusal of nether run and bounded evaluation fuel (§6.4 and §8.0, crates/nether-cli/tests/rites.rs and crates/nether-bury/tests/collapse.rs).

Tier 3 — Believed or open (neither proved nor closed)

These claims are relied on as assumptions or tracked as open items in cairn/items/; none is claimed as proved or finished:

Cryptographic collision resistance of BLAKE3 (§7.2): proof/encoding.py proves that the domain-separated preimage b"netherc/cairn/v4\x00" ++ encode(x) is injective; that distinct preimages produce distinct 32-byte cairns rests on the standard cryptographic assumption on BLAKE3 and is not proved here.
Making invalid in-memory Value and Node states unrepresentable in Rust types (0115): until 0115 lands, well-formedness side conditions (such as origin ≤ 8 on Value::Shade, non-empty struct and callee names, and Span.start ≤ Span.end) are enforced by codec::encode_* and codec::decode_* checks rather than private constructors.
Two-machine independent verification of a tagged release binary (0221): the reproducible build recipe (scripts/task release:build with --remap-path-prefix and --locked) is in the tree, and the two-host tag attestation remains open until a release tag is built and compared across two independent machines.
Remaining open roadmap items, among them 0075 (the trace graph browser), 0078 (a stranger explains a hole), 0081 and 0082 (the second and third projections), 0103 (a pilot), 0104 (an introduction), 0105 (a conformance suite), 0106 (a public store), 0108 (a 24-hour decoder soak), 0210 (a year of a real store), and 0235 (the face for other users). cairn list is the full list.