Skip to content

Commit 3b44dbb

Browse files
docs: record tech-debt audit findings (2026-05-26) (#74)
## Summary - Adds `docs/tech-debt-2026-05-26.md` with this repo's findings from the estate-wide tech-debt scan. - Covers proof debt, licence debt, documentation debt — with per-section severity. ## What this PR does NOT do This file records findings. It does not close the debt. Each section has a "Recommended next move" line; closing the debt is follow-up work. ## Companion estate-wide audits - hyperpolymath/standards#195 — proof-debt audit - hyperpolymath/standards#196 — licence-debt audit - hyperpolymath/standards#197 — documentation-debt audit 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 893d07f commit 3b44dbb

1 file changed

Lines changed: 73 additions & 0 deletions

File tree

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

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
4+
-->
5+
6+
# Tech-Debt Audit — proof-of-work — 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:** `MEDIUM`.
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= 3 | Unsafe= 0
20+
```
21+
22+
**Total markers:** 3. **Severity:** `>03`.
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 | 131 |
53+
| `docs/` files | 2 |
54+
| `docs/` LoC | 653 |
55+
| CHANGELOG.md | N |
56+
| CONTRIBUTING.md | Y |
57+
| CODE_OF_CONDUCT.md | Y |
58+
| SECURITY.md | Y |
59+
| Severity | `MEDIUM` |
60+
61+
**Recommended next move:** introduce a `docs/` directory. The README at 131 lines has likely grown to do the work of `docs/` — split it into a thin README + `docs/architecture.md`, `docs/usage.md`, etc. Heavy-wiki exemplars to copy from: `affinescript`, `boj-server`, `echidna`, `hypatia`.
62+
63+
Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up.
64+
65+
## Cross-references
66+
67+
- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md`
68+
- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md`
69+
- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md`
70+
71+
---
72+
73+
🤖 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)