|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += Tech-Debt Audit — rsr-template-repo — 2026-05-26 |
| 4 | + |
| 5 | +*Source:* estate-wide automated scan 2026-05-26. |
| 6 | +*Companion:* https://github.com/hyperpolymath/standards/tree/main/docs/audits[`hyperpolymath/standards` 2026-05-26-estate-*-debt audits]. |
| 7 | +*Combined severity:* `LOW`. |
| 8 | + |
| 9 | +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. |
| 10 | + |
| 11 | +== 1. Proof debt |
| 12 | + |
| 13 | +Scanner counted the following markers in proof-bearing files of this repo: |
| 14 | + |
| 15 | +---- |
| 16 | +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 |
| 17 | +---- |
| 18 | + |
| 19 | +*Total markers:* 6. *Severity:* `>06`. |
| 20 | + |
| 21 | +*Marker types* (any non-zero counts above): |
| 22 | +* Coq `Axiom`/`Admitted` — unconditional proof escapes. |
| 23 | +* Lean `sorry`/`axiom` — Lean's equivalent. |
| 24 | +* Agda `postulate` — accepted axiomatically. |
| 25 | +* Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. |
| 26 | +* Idris2 top-level `partial` — totality-check waived. |
| 27 | +* F\* `assume val`/`admit_p` — F\* admit. |
| 28 | +* `TODO PROOF` / `OWED:` — self-documented debt markers. |
| 29 | +* `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. |
| 30 | + |
| 31 | +*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`. |
| 32 | + |
| 33 | +== 2. Licence debt |
| 34 | + |
| 35 | +[cols="1,1",options="header"] |
| 36 | +|=== |
| 37 | +|Field |Value |
| 38 | +|LICENSE file |`LICENSE` |
| 39 | +|SPDX header |`MPL-2.0` |
| 40 | +|Manifest licence |`NONE` |
| 41 | +|Body classifier |`Palimp-MPL-2.0` |
| 42 | +|Severity |`ok` |
| 43 | +|=== |
| 44 | + |
| 45 | + |
| 46 | +*Recommended next move:* none for licence. |
| 47 | + |
| 48 | +== 3. Documentation debt |
| 49 | + |
| 50 | +[cols="1,1",options="header"] |
| 51 | +|=== |
| 52 | +|Field |Value |
| 53 | +|README lines |186 |
| 54 | +|`docs/` files |70 |
| 55 | +|`docs/` LoC |4218 |
| 56 | +|CHANGELOG.md |Y |
| 57 | +|CONTRIBUTING.md |N |
| 58 | +|CODE_OF_CONDUCT.md |N |
| 59 | +|SECURITY.md |N |
| 60 | +|Severity |`OK` |
| 61 | +|=== |
| 62 | + |
| 63 | + |
| 64 | +*Recommended next move:* none for docs. |
| 65 | + |
| 66 | +== Cross-references |
| 67 | + |
| 68 | +* Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` |
| 69 | +* Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` |
| 70 | +* Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` |
| 71 | + |
| 72 | +''' |
| 73 | + |
| 74 | +🤖 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