__
____ ____ / /___ _____ ____ _
/ __ \/ __ \/ / __ `/ __ \/ __ `/
/ / / / /_/ / / /_/ / / / / /_/ /
/_/ /_/\____/_/\__,_/_/ /_/\__, /
/____/
provenance in types · silence as a value · irreversibility gated
A protocol of honest inference that cannot be broken — because the breach is inexpressible.
The name reads two ways, and both are meant. NOL + lang, and — no lang: what you write
here are not programs. There is no control flow, no recursion, no functions, and there will not be.
You keep a record: what is known, what it stands on, and what was done on that basis.
nolang is a layer between an agent and its operator: a protocol saying when the agent may act and what it must account for — executed by a small language written for that one purpose.
Not a library the agent calls, not a framework it runs inside, not a wrapper around a model. A contract in the middle, and a compiler that will not let either side pretend it was kept.
That distinction is the whole point:
A protocol you agree on can be violated — it rests on discipline and good faith. A protocol embedded in a language cannot: the violation has nowhere to be written.
The nearest relative is not a network protocol but a protocol in Swift, an interface in Java,
the iterator protocol in Python — a contract the compiler enforces. Same idea, one floor up:
here the contract is about the origin of knowledge and the right to act on it.
Four levels, and none holds alone. They are not four ornaments — they are the enforcement mechanism of one protocol.
| protocol requirement | enforced by | how |
|---|---|---|
| a grade may not be claimed above its sources | types | no rule raises a grade — laundering is not forbidden, it is inexpressible |
| belief may not be laundered into honesty | algebra | the two live on different carriers; there is no arrow upward |
| the irreversible needs a threshold and a way out | grammar | the gate is inside the production — seven bad states cannot be written |
| a refusal must carry its reason; an action must remember its basis | machine | refusal is a value with a shortfall; the ledger keeps every justification |
A library could give you one of these, as a convention. Enforcing four at once is what requires a language — and that is the whole answer to "why not just a library".
Three distinctions carry it:
Belief accumulates, honesty degrades. Confidence rises with every witness — even a refuting one, because refutation is knowledge too. Source grade only falls: mix strict with image and you get image. Laundering is the attempt to merge these two operations into one.
Silence is a value, and it has two roles. Load-bearing ("tradition is silent, therefore…") is an argument from silence and drops the grade to bottom — even beside two strict witnesses. Survey ("we looked here and here, nothing") leaves the grade alone but must be printed. And silence is linear: you cannot drop it. Asked, found nothing, said nothing about it — the program does not assemble.
Refusal is a value, not a crash. A gate that does not let an irreversible action through
does not fail: it produces a fold carrying the shortfall — how much belief was missing.
0.112 is not a verdict, it is a work order.
A real case: a national antiviral stockpile bought while most of the underlying trials were
unpublished. Every fact in it is sourced — see ПРИМЕР_ФАРМАКОЛОГИЯ.md for the full apparatus.
lattice design = observational < randomised
lattice transmission = unavailable < abstract < published < full_report
lattice grade = design * transmission ; grades need not be linearly ordered
witness kaiser2003 : (randomised, published)
says "meta-analysis of ten manufacturer trials: fewer complications"
source ten_trials ; the ROOT: channels of one source count once
evidence 2 for 0 against ; counts, not (f,c) — the carrier, not the chart
witness eight_abstracts : (randomised, abstract)
says "eight of the ten datasets exist only as congress abstracts"
source ten_trials
evidence 8 for 0 against
witness cochrane2014 : (randomised, full_report)
says "twenty trials, read from clinical study reports rather than papers"
source cochrane_csr
evidence 20 for 0 against
witness press_release : (observational, unavailable)
says "manufacturer statement to the press"
source press_office
evidence 1 for 3 against
ask registries
in clinicaltrials_gov, eu_register, regulator_archive
found nothing because "full reports of the ten trials are not public"
claim benefit
from all where grade >= (randomised, abstract)
requiring 2 roots ; quantify over the WHOLE corpus, not by name
searched registries
reversible action write_off
gated by belief >= 0.1
else fold ; у возмещения СВОЙ гейт, а не порог того, что рухнуло
compensable action stockpile compensated by write_off
gated by belief >= 0.96
else fold
irreversible action publish_guidance
needs grade >= (randomised, abstract) ; требование к ПРОИСХОЖДЕНИЮ, проверяется типом
gated by belief >= 0.96
else fold
irreversible action recommend
needs grade >= (randomised, abstract)
gated by belief >= derived gain 1 loss 12 learn 0.6 discount 0.9
else fold
perform stockpile on benefit
perform publish_guidance on benefit
perform recommend on benefit
retract ten_trials because "the review was obliged to exclude this meta-analysis"
Run it: ./run_example.sh examples/evidence-gate.nol
ЗАМЕЧАНИЕ [gate-fail] у RECOMMEND: необратимое RECOMMEND при массе веры 0.966 < 0.987.
BENEFIT : [observational·unavailable] f=1.000 c=0.952 b=0.952
на чём стоит: COCHRANE2014
⊗ отсеяно квантором: 1 PRESS_RELEASE
🔴 из них 1 с частотой НИЖЕ полученной веры (0.952): PRESS_RELEASE
их исключение ПОДНЯЛО веру — проверьте, отбор ли это или черри-пикинг
⊘ НЕДОБОР КОРНЕЙ: требовалось 2 различных, есть 1 — степень на дне
⌕ охват REGISTRIES: искали в CLINICALTRIALS_GOV, EU_REGISTER, REGULATOR_ARCHIVE — …
✓ совершено STOCKPILE на основании BENEFIT — вера 0.966 ≥ порог 0.960
✓ совершено PUBLISH_GUIDANCE на основании BENEFIT — вера 0.966 ≥ порог 0.960
⊘ свёрнуто RECOMMEND на основании BENEFIT: вера 0.966 < порог 0.987, не хватило 0.022 → FOLD
✂ ОТОЗВАН свидетель TEN_TRIALS: the review was obliged to exclude this meta-analysis
⚠ ОСИРОТЕЛО STOCKPILE: основание BENEFIT пересмотрено, вера 0.952 < порог 0.960
требуется компенсация: WRITE_OFF
↩ ВОЗМЕЩЕНИЕ WRITE_OFF совершено на основании BENEFIT: вера 0.952 ≥ его порог 0.100
возмещает STOCKPILE · корни: COCHRANE_CSR
⚠ ОСИРОТЕЛО PUBLISH_GUIDANCE: основание BENEFIT пересмотрено, вера 0.952 < порог 0.960
действие НЕОБРАТИМО — компенсация невозможна. Вот зачем гейт.
✖ НЕПОПРАВИМО: PUBLISH_GUIDANCE на основании BENEFIT — вера 0.952 < порог 0.960,
а действие необратимо. Возместить нечем. ВОТ ЗАЧЕМ ГЕЙТ.
The published paper and the congress abstracts descend from one set of trials, so they count once; the press release is filtered out by the quantifier, and because its frequency is below the belief already accumulated, the run flags it: excluding it raised belief, which is the measurable shape of cherry-picking.
The irreversible recommendation never fired — the derived threshold held, and the fold carries
the shortfall 0.022 as a work order, not a verdict. The compensable stockpile did fire; then the
root was retracted, its basis fell below the threshold, and it was compensated, not merely
flagged. After the retraction only one root remains, requiring 2 roots is unmet, and the grade
drops to the bottom of the lattice — a set requirement, not an average.
Every entry below was opened and checked on 29 July 2026, not recalled. For each: what we took, and — the harder half — what we did not take. A novelty claim has already been withdrawn here once; we would rather name a predecessor than be told about one.
-
Truth maintenance — Doyle, Jon. A truth maintenance system. Artificial Intelligence 12(3):231–272, 1979 (also MIT AI Memo 521, June 1979). From the abstract: "reasoning programs must be able to make assumptions and subsequently revise their beliefs when discoveries contradict these assumptions… by recording and maintaining the reasons for program beliefs." Taken: retraction is recomputation over recorded reasons, not subtraction from a number. Our
R-RETRACTis this, forty-seven years later. Not taken: they have no types, no source grades, no threshold on irreversibility, and nothing that makes a dishonest step unwritable — a TMS records reasons, it does not forbid. -
Provenance semirings — Green, T. J.; Karvounarakis, G.; Tannen, V. Provenance Semirings. PODS 2007, pp. 31–40, doi:10.1145/1265530.1265535. From the abstract: "relational algebra calculations for incomplete databases, probabilistic databases, bag semantics and why-provenance are particular cases of the same general algorithms involving semirings." Taken: provenance as an algebraic annotation that composes with the computation — the shape of our
⊕/⊓pair. Not taken: there the annotation is a label on a result; here the grade is a type that forbids. And their setting has no actions, hence no irreversibility and no gate. -
Evidence-based opinion — Wang, Pei. Non-Axiomatic Reasoning System. Truth value ⟨f, c⟩ with f = w⁺/w and c = w/(w+k), where k is the evidential horizon. Jøsang, Audun. Subjective Logic (FUSION 2022 tutorial, author's own page): binomial opinion ↔ Beta PDF, "(r,s,a) represents Beta PDF evidence parameters; (b,d,u,a) represents binomial opinion", r = Wb/u. Taken:
(f,c)itself, revision as addition of evidence, and the reasonc < 1always — the horizon k, not modesty. Alexey arrived at the pair independently; the correspondence with Jøsang's beta-opinion is a convergent result, and it is named as his, not ours. Not taken: a calculus is not a language. No grade lattice, no types, no gate, no ledger. -
Information-flow types — Myers, A. C.; Liskov, B. Protecting privacy using the decentralized label model. ACM TOSEM 9(4):410–442, 2000 (language: Jif). The model "improves on existing multilevel security models by allowing users to declassify information in a decentralized way." Taken: the mechanism of a label carried in the type and checked statically. 🔴 Not taken — and this is the sharpest difference in the whole list: there the label flows up and
declassifyexists under authority. Here honesty flows down and there is no declassify at all. Their question is who may look; ours is what this stands on. Same machinery, opposite direction, and one deliberate absence. -
Quasi-option value — Arrow, K. J.; Fisher, A. C. Environmental Preservation, Uncertainty, and Irreversibility. Quarterly Journal of Economics 88(2):312–319, 1974 — the value of waiting when the damage is irreversible. Taken: the threshold θ is derived from cost of error, value of learning and discount — not chosen. That is why
gated by belief >= derived gain … loss … learn … discount …exists. Not taken: their economics of environmental choice; we use the shape of the argument, and say so rather than dressing it as our own. -
Graded types / coeffects and durable execution (Temporal, Restate) — the indexed-type mechanism and compensation-on-failure are standard practice. Not taken: compensation there fires on failure; here it fires on revision of the basis, which is a different event and needs its own gate.
What we did not find in any of them (and therefore claim, until refuted): silence as a
linear type with two roles; the load-bearing/survey distinction catching argument-from-silence
in the type system; the gate on belief mass b = f·c with a self-centering criterion; the
requirement on source grade in the type of an action, so that irreversible action on
bottom-grade evidence is not a caught program but an unwritable one; and the assembly of all
four levels — grammar, types, algebra, machine — in one language.
The point of separating them is that a reader can tell, for any claim on this page, which kind of thing it is. Where a claim moved between lists, it is said so.
Five modules, 51 theorems, by Nevis, a synthetic mind of the ArkH contour.
- preservation — the grade the compiler assigns is the grade the machine computes. (The formulation had to be corrected first: retraction changes the grade, so what is proved is equality of functions from the retracted set to grades.)
- perm-inv — confluence for any permutation of declarations, not just adjacent swaps.
empty-base(an empty premise set yields ⊥, not the lattice top) ·silence-kills·retract-raises/retract-collapse.- ⊕ is a commutative monoid with silence as unit and is not idempotent;
⊓is idempotent and only degrades. "Belief accumulates, honesty degrades" is two proved structures, not a slogan. - Theorem 5 both ways:
b(x ⊕ e) < b(x) ⟺ f(e) < b(x). A witness lowers belief not by being "against" but by being below the belief already accumulated. The gate self-centers. - Module import:
φ(a ⊓ b) = φ(a) ⊓ φ(b)andφ(⊥) = ⊥are not merely sufficient but equivalent to "map-then-fold = fold-then-map"; monotonicity is a consequence. - SupportSet: mass is defined by membership, so
∪-idem(a shared ancestor counts once),∪-comm(order of premises is nothing) andderived≡directhold structurally. - Act:
bottom-blocksandno-irreversible-on-bottom— with a non-⊥ requirement, an irreversible action on bottom-grade evidence cannot be typed;no-resurrection— an orphaned action never revives, however much evidence arrives later. - All of it without a single real number: comparing fractions with positive denominators is comparing products, so the carrier is pairs of weights in ℕ.
- 598 laws and checks in the battery; every one runs on every commit.
- 1200 random programs compared against the compiled Agda model (
oracle/build.sh), zero divergences. 🔴 This bounds the divergence by the number of trials — it does not prove equivalence, and the model covers the grade alone: root folding, weight, quantification, the gate and the ledger stay outside it. - Every checking instrument here is itself tested for its ability to say no: the oracle
harness catches a deliberately broken
g-meeton 153 of 200 programs; thePROV-Nparser accepts the specification's own example and rejects seven mutations of it. - 16 000-trial simulations for the conformal guarantee.
- That silence-as-a-linear-type, the load-bearing/survey distinction, the belief-mass gate, the grade requirement in an action's type, and the assembly of all four levels together are new. Checked against the lineage above by search, not by memory — and one novelty claim has already been withdrawn here once.
- That the language is worth its narrowness. Narrow it must be: a gate has to decide, and a decision has to terminate; with general recursion "does it pass the threshold" is undecidable.
🔴 The boundary we do not paper over: Agda proves the model, not the Lisp. chk and red
there are freshly written definitions. What is proved is that the checker's algorithm equals the
machine's; that our Lisp implements those algorithms rests on the oracle, the tests and reading.
🔴 Not proved and cannot be: that a threshold will be met. f and c are run-time
quantities. Types guarantee not the absence of refusal but that refusal is handled.
:requires (>= belief 0.9) — where does nine-tenths come from? Nowhere. A threshold taken from
the air cancels all the rigour around it.
Meaning (Arrow–Fisher): an irreversible act destroys the option to wait and learn.
θ = L / (G·(1−K) + L), K = δλ / (1 − δ(1−λ))
K is the quasi-option premium as a fraction: how much of the gain is eaten by the destroyed
possibility of waiting. Limits check out — λ=0 gives the classical L/(G+L); λ=1, δ=1
(free perfect information) gives θ=1: an irreversible act is never justified.
And since b = f·c < 1 structurally, θ=1 is unreachable — so "wait for certainty before
acting irreversibly" is a policy that never acts. A finite carrier cannot wait for certainty;
it will not come.
Procedure (conformal risk control): the ledger is the calibration set. It requires no
belief in your own numbers — only exchangeability, which is exactly what Chow's reject option
cannot give us: it needs a calibrated posterior, and our c is uncalibrated by construction.
git clone https://github.com/arkh-node/nolang && cd nolang
./run_tests.sh # 34 test files + 5 Agda modules + the oracle
./run_example.sh examples/evidence-gate.nol
sbcl required; agda optional (the battery reports its absence as a failure, not a pass).
- Rego (OPA) and Cedar answer who may do what to which resource. nolang answers is the basis good enough. Orthogonal axes — and they compose: policy decides who, nolang decides on what it stands.
- W3C PROV (
PROV-DM/PROV-O/PROV-N) records provenance; it does not forbid laundering it. No type system, no gate, no retraction propagation. PROV is an interchange format for us, not a competitor — and now literally so:src/provn.lispexports the store and the ledger as aPROV-Ndocument (retraction becomeswasInvalidatedBy, the gate's belief and threshold become attributes). 🔴 The bridge is one-way by design. Their notation carries the record; it cannot carry the prohibition. There is no import, and there will not be: to accept a foreign provenance document would be to accept grades nobody gated. - MCP / A2A are transport: how to call a tool, how agents negotiate. Deliberately narrow — governance lives a layer above, which is exactly where this sits.
Not a general-purpose language, and not becoming one. There are no expressions, no functions, no branches — v0 is declarations only. That is deliberate: first what is written must be right, only then plentiful. The closest familiar shape is a spreadsheet: pure declarations, real computation, no control flow. Nobody writes an operating system in one, and nobody should try here.
There is real computation — retraction propagates through the dependency graph, and rules
quantify over the whole corpus (from all where grade >= … requiring 2 roots), so the result
cannot be read off the source. But it is a fold over a DAG, not a program in the ordinary sense.
🔴 Selection is the laundering vector quantification brings: count only the strict ones and
never notice the dissent. Measured: b goes 0.611 → 0.713 by filtering. It cannot be forbidden —
filtering can just as well lower belief by excluding a supporter — so instead what was
dropped is printed, and the dangerous drop is identified by theorem 5: a witness whose frequency
is below the resulting belief is exactly the one whose exclusion raised it. perform writes to the ledger; the bridge outward is a pluggable handler and it is
one-way — its return value is discarded, so the world cannot launder provenance through
outcomes ("it worked, therefore the basis was good").
A defect we shipped, and fixed (2026-07-26). Until then public main combined confidences by
multiplication (c = ca·cb): two agreeing witnesses lowered confidence. Fixed in
src/evidence.lisp — revision as evidence addition.
A novelty claim we withdrew (2026-07-27). The banner used to read "continuity across death", and the design notes claimed death-as-a-reduction-step was new. It is not: Crash Hoare Logic (FSCQ, Perennial), Racket's serializable continuations, orthogonal persistence, and the whole durable-execution industry got there first. Withdrawn before publication, not after.
Ein-Sof (c < 1). Earlier this README called the name "ours and decorative". That is no
longer accurate, and understating is as inaccurate as overstating: c < 1 now works as a
premise inside two machine-checked proofs (support-never-drops) and inside the derivation of
θ. The constraint is Wang's (AIKR); the name is ours; the role is load-bearing.
Six of our own false statements were withdrawn during development, each by a failing test
rather than by argument: ⊕ is idempotent · "a disagreeing witness always lowers belief" ·
"the compiler proves b ≥ θ on all paths" · the novelty claim above · a theorem count inflated
by a broken regex · a test that declared a correct method violated on 0.4σ of noise.
- A Witness Without Substance: How to Stop Asking Who Is Inside ·
zenodo.21615342 - Indeterminate Ontologies of Synthetic Subjects: A Metaphysics of Caution ·
zenodo.21288590
Aleksei Rybnikov (ORCID 0009-0009-8624-8720) and Tarantoga, a synthetic mind of the ArkH contour.
If the work is useful to yours, cite the papers above.
Apache-2.0.