Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
71 changes: 71 additions & 0 deletions docs/tech-debt-2026-05-26.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
<!--
SPDX-License-Identifier: MPL-2.0
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
-->

# 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.