Skip to content

docs: an Applications-in-practice section #189

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Oct 15, 2026
Merged

docs: an Applications-in-practice section #189

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
541ec8f
docs: an Applications-in-practice section -- the discipline earned on…
hyperpolymath Oct 15, 2026
fff398a
docs: the typed CNO/OND treatment is the model checked here, not the …
hyperpolymath Oct 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 40 additions & 0 deletions docs/COOKBOOK.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -741,3 +741,43 @@ 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. 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) -- 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 account of exactly the paths where the damage never
reaches a log.
Loading