Skip to content

Commit 07a6233

Browse files
docs: record tech-debt audit findings (2026-05-26) (#18)
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) <noreply@anthropic.com>
1 parent 24a2130 commit 07a6233

1 file changed

Lines changed: 71 additions & 0 deletions

File tree

docs/tech-debt-2026-05-26.md

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
-->
5+
6+
# Tech-Debt Audit — proof-burrower — 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= 19 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
20+
```
21+
22+
**Total markers:** 6. **Severity:** `>06`.
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 | `MPL-2.0` |
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 | 186 |
53+
| `docs/` files | 62 |
54+
| `docs/` LoC | 4015 |
55+
| CHANGELOG.md | Y |
56+
| CONTRIBUTING.md | Y |
57+
| CODE_OF_CONDUCT.md | Y |
58+
| SECURITY.md | Y |
59+
| Severity | `OK` |
60+
61+
**Recommended next move:** none for docs.
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

Comments
 (0)