From 541ec8f37698d89e8daeace5407a926e7887bc79 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 10:31:56 +0100 Subject: [PATCH 1/2] docs: an Applications-in-practice section -- the discipline earned on a real pipeline Appends a worked real-world case to docs/COOKBOOK.adoc: the concrete situation in an amplicon-sequencing pipeline in production use where the type, the OND discipline or the algebra earns its keep -- and what the untyped or undisciplined alternative gets wrong. Documentation only; no code changes. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- docs/COOKBOOK.adoc | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/docs/COOKBOOK.adoc b/docs/COOKBOOK.adoc index a462373..b225b32 100644 --- a/docs/COOKBOOK.adoc +++ b/docs/COOKBOOK.adoc @@ -741,3 +741,32 @@ See `LICENSE-AGPL3.md` and `LICENSE-PALIMPSEST.md` for details. _Last updated: 2025-11-22_ _Status: Proofs verified ✓ | Theorems established ✓ | More work to do ✓_ + +== Applications in practice + +The pillars earn their keep on real reporting rules. Two worked cases from +MetaManifold (https://github.com/JoshuaJewell/MetaManifold-WebUI), an +amplicon-sequencing pipeline in production use: + +* *OND, the disclosure side.* Its significance tests carry a status: +`:computed`, `:r_unavailable`, `:no_paired_samples`, `:test_failed`. The +engineering rule the app enforces by tests is exactly an OND claim -- a +result whose test did not run reveals nothing, and must never be published +as a null result. Modelled with the OND discipline, the statuses become a +type: the numbers exist only in the constructor whose status is `computed`, +and a "publish" function requires evidence the test ran. The untested branch +cannot produce a number at all; the typechecker refuses it, where a test can +only assert it. + +* *CNO, the operation side.* The app refuses to fit a negative-binomial GLM +when one group has no reads at all (complete separation): the fold change +is unbounded and the Wald p-value collapses towards 1 despite reported +convergence. That refusal is a CNO in the flesh -- the degenerate fit is an +operation that provably computes nothing of value, and certifying it as +null turns a guarded code path into a typed guarantee that the funny +result can never be produced. + +The real-world value is where tests are weakest: the silent failure paths. +A user asking "is this safe and sound, or will it produce funny results?" +gets a machine-checked answer for exactly the paths where the damage never +reaches a log. From fff398a853b05cfe06dde210bea20141f1e3ef53 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 10:49:49 +0100 Subject: [PATCH 2/2] docs: the typed CNO/OND treatment is the model checked here, not the app's code (CodeRabbit, PR #189) The section read as though MetaManifold already provides a typed machine-checked guarantee; its implementation enforces both rules with status symbols and guarded control flow, held by tests. The passage now says that plainly, names the type-level treatment as the modelled endpoint checked in this repository (proofs/agda/OND.agda, proofs/agda/CNO.agda), and links the concrete app-side artifacts at their pins: the status logic in src/analysis/analysis.jl (7d5e9a4) and the complete-separation refusal asserted in test/unit/test_differential.jl. The closing sentence claims a machine-checked account of the failure paths, not a machine-checked answer shipped by the app. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- docs/COOKBOOK.adoc | 47 ++++++++++++++++++++++++++++------------------ 1 file changed, 29 insertions(+), 18 deletions(-) diff --git a/docs/COOKBOOK.adoc b/docs/COOKBOOK.adoc index b225b32..ed13ae2 100644 --- a/docs/COOKBOOK.adoc +++ b/docs/COOKBOOK.adoc @@ -746,27 +746,38 @@ _Status: Proofs verified ✓ | Theorems established ✓ | More work to do ✓_ The pillars earn their keep on real reporting rules. Two worked cases from MetaManifold (https://github.com/JoshuaJewell/MetaManifold-WebUI), an -amplicon-sequencing pipeline in production use: - -* *OND, the disclosure side.* Its significance tests carry a status: -`:computed`, `:r_unavailable`, `:no_paired_samples`, `:test_failed`. The -engineering rule the app enforces by tests is exactly an OND claim -- a -result whose test did not run reveals nothing, and must never be published -as a null result. Modelled with the OND discipline, the statuses become a -type: the numbers exist only in the constructor whose status is `computed`, -and a "publish" function requires evidence the test ran. The untested branch -cannot produce a number at all; the typechecker refuses it, where a test can -only assert it. +amplicon-sequencing pipeline in production use. In the app today both rules +are enforced engineering: status symbols and guarded code paths, held by +tests. What this repository adds is the machine-checked account of *why +those rules are the right ones* -- +link:../proofs/agda/OND.agda[OND.agda] and +link:../proofs/agda/CNO.agda[CNO.agda] -- and the type-level treatment they +model. The typed form is the proposal, checked here; it is not a claim +about the app's present code. + +* *OND, the disclosure side.* MetaManifold's significance tests carry a +status: `:computed`, `:r_unavailable`, `:no_paired_samples`, `:test_failed` +(https://github.com/hyperpolymath/MetaManifold-WebUI/blob/7d5e9a4/src/analysis/analysis.jl[src/analysis/analysis.jl], +pinned on the fork's `main` at 7d5e9a4). The engineering rule the app +enforces by tests is exactly an OND claim -- a result whose test did not +run reveals nothing, and must never be published as a null result. Modelled +with the OND discipline, the statuses become a type: the numbers exist only +in the constructor whose status is `computed`, and a "publish" function +requires evidence the test ran. The untested branch cannot produce a number +at all; the typechecker refuses it, where a test can only assert it. * *CNO, the operation side.* The app refuses to fit a negative-binomial GLM -when one group has no reads at all (complete separation): the fold change -is unbounded and the Wald p-value collapses towards 1 despite reported -convergence. That refusal is a CNO in the flesh -- the degenerate fit is an -operation that provably computes nothing of value, and certifying it as -null turns a guarded code path into a typed guarantee that the funny -result can never be produced. +when one group has no reads at all (complete separation) -- asserted by +https://github.com/hyperpolymath/MetaManifold-WebUI/blob/7d5e9a4/test/unit/test_differential.jl[test/unit/test_differential.jl]: +the fold change is unbounded and the Wald p-value collapses towards 1 +despite reported convergence. That refusal is a CNO in the flesh -- the +degenerate fit is an operation that provably computes nothing of value, +which is what link:../proofs/agda/CNO.agda[CNO.agda] machine-checks. +Certifying it as null would turn a guarded code path into a typed +guarantee that the funny result can never be produced; that typed +guarantee is the modelled endpoint, not the app's implementation. The real-world value is where tests are weakest: the silent failure paths. A user asking "is this safe and sound, or will it produce funny results?" -gets a machine-checked answer for exactly the paths where the damage never +gets a machine-checked account of exactly the paths where the damage never reaches a log.