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.