From c2cca62d252e96ae9227e4cc221dfb70833d26a2 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 12:52:22 +0100 Subject: [PATCH] docs: record tech-debt audit findings (2026-05-26) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds docs/tech-debt-2026-05-26.md with this repo's findings from the estate-wide tech-debt scan: proof debt, licence debt, documentation debt. This file records the findings only — it does not close the debt. Cross-references: - hyperpolymath/standards#195 (estate proof-debt audit) - hyperpolymath/standards#196 (estate licence-debt audit) - hyperpolymath/standards#197 (estate documentation-debt audit) Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/tech-debt-2026-05-26.md | 71 ++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 docs/tech-debt-2026-05-26.md diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md new file mode 100644 index 0000000..f1f4030 --- /dev/null +++ b/docs/tech-debt-2026-05-26.md @@ -0,0 +1,71 @@ + + +# Tech-Debt Audit — natsci-studio — 2026-05-26 + +**Source:** estate-wide automated scan 2026-05-26. +**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). +**Combined severity:** `LOW`. + +This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. + +## 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this repo: + +``` +files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +``` + +**Total markers:** 6. **Severity:** `>06`. + +**Marker types** (any non-zero counts above): +- Coq `Axiom`/`Admitted` — unconditional proof escapes. +- Lean `sorry`/`axiom` — Lean's equivalent. +- Agda `postulate` — accepted axiomatically. +- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. +- Idris2 top-level `partial` — totality-check waived. +- F\* `assume val`/`admit_p` — F\* admit. +- `TODO PROOF` / `OWED:` — self-documented debt markers. +- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. + +**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. + +## 2. Licence debt + +| Field | Value | +|---|---| +| LICENSE file | `LICENSE` | +| SPDX header | `AGPL-3.0-or-later` | +| Manifest licence | `NONE` | +| Body classifier | `Palimpsest-some` | +| Severity | `ok` | + +**Recommended next move:** none for licence. + +## 3. Documentation debt + +| Field | Value | +|---|---| +| README lines | 53 | +| `docs/` files | 55 | +| `docs/` LoC | 2437 | +| CHANGELOG.md | Y | +| CONTRIBUTING.md | Y | +| CODE_OF_CONDUCT.md | Y | +| SECURITY.md | Y | +| Severity | `OK` | + +**Recommended next move:** none for docs. + +## Cross-references + +- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` +- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` +- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` + +--- + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.