|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: MPL-2.0 |
| 3 | +SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) |
| 4 | +--> |
| 5 | + |
| 6 | +# Tech-Debt Audit — panic-attack — 2026-05-26 |
| 7 | + |
| 8 | +**Source:** estate-wide automated scan 2026-05-26. |
| 9 | +**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). |
| 10 | +**Combined severity:** `LOW`. |
| 11 | + |
| 12 | +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. |
| 13 | + |
| 14 | +## 1. Proof debt |
| 15 | + |
| 16 | +Scanner counted the following markers in proof-bearing files of this repo: |
| 17 | + |
| 18 | +``` |
| 19 | +files= 3 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 9 |
| 20 | +``` |
| 21 | + |
| 22 | +**Total markers:** 9. **Severity:** `>09`. |
| 23 | + |
| 24 | +**Marker types** (any non-zero counts above): |
| 25 | +- Coq `Axiom`/`Admitted` — unconditional proof escapes. |
| 26 | +- Lean `sorry`/`axiom` — Lean's equivalent. |
| 27 | +- Agda `postulate` — accepted axiomatically. |
| 28 | +- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. |
| 29 | +- Idris2 top-level `partial` — totality-check waived. |
| 30 | +- F\* `assume val`/`admit_p` — F\* admit. |
| 31 | +- `TODO PROOF` / `OWED:` — self-documented debt markers. |
| 32 | +- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. |
| 33 | + |
| 34 | +**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`. |
| 35 | + |
| 36 | +## 2. Licence debt |
| 37 | + |
| 38 | +| Field | Value | |
| 39 | +|---|---| |
| 40 | +| LICENSE file | `LICENSE` | |
| 41 | +| SPDX header | `MPL-2.0` | |
| 42 | +| Manifest licence | `NONE` | |
| 43 | +| Body classifier | `Palimp-MPL-2.0` | |
| 44 | +| Severity | `ok` | |
| 45 | + |
| 46 | +**Recommended next move:** none for licence. |
| 47 | + |
| 48 | +## 3. Documentation debt |
| 49 | + |
| 50 | +| Field | Value | |
| 51 | +|---|---| |
| 52 | +| README lines | 220 | |
| 53 | +| `docs/` files | 12 | |
| 54 | +| `docs/` LoC | 2839 | |
| 55 | +| CHANGELOG.md | Y | |
| 56 | +| CONTRIBUTING.md | Y | |
| 57 | +| CODE_OF_CONDUCT.md | Y | |
| 58 | +| SECURITY.md | Y | |
| 59 | +| Severity | `LOW` | |
| 60 | + |
| 61 | +**Recommended next move:** `docs/` has only 12 file(s). Aim for ≥10 organised docs (architecture, usage, contributing-guide, troubleshooting, design-decisions). The user's bar for a "heavily-developed and well-organised wiki" is ≥10 files with topical organisation. |
| 62 | + |
| 63 | +## Cross-references |
| 64 | + |
| 65 | +- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` |
| 66 | +- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` |
| 67 | +- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` |
| 68 | + |
| 69 | +--- |
| 70 | + |
| 71 | +🤖 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. |
0 commit comments