|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | + |
| 4 | += Ecosystem Status — Musts / Intends / Wishes |
| 5 | +Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 6 | +:revdate: 2026-06-19 |
| 7 | +:revnumber: 1.0 |
| 8 | +:toc: left |
| 9 | +:sectnums: |
| 10 | + |
| 11 | +[.lead] |
| 12 | +A point-in-time status of four hyperpolymath projects, each grouped into the |
| 13 | +normative tiers *MUST* (invariants / required), *INTEND* (declared, in-progress), |
| 14 | +and *WISH* (aspirational). JtV is the normative anchor. |
| 15 | + |
| 16 | +Legend: ✅ done · ◑ partial · ◻ planned · ⚠ gap · ○ aspirational. |
| 17 | + |
| 18 | +Sources / freshness: JtV is live (this session, commit `fff9689`); Absolute Zero |
| 19 | +from `STATE.a2ml` (2026-05-27); JanusKey from `STATE.a2ml` (2026-04-04, older) + |
| 20 | +README; maa-framework not yet in working scope (see §5). |
| 21 | + |
| 22 | +== JtV — the normative anchor |
| 23 | + |
| 24 | +Harvard-architecture language: Control (Turing-complete) vs Data (Total, |
| 25 | +addition-only); code injection grammatically impossible. Echo + Epistemic effect |
| 26 | +system for reversibility / structured loss. |
| 27 | + |
| 28 | +[cols="1,5,3",options="header"] |
| 29 | +|=== |
| 30 | +| Tier | Item | Where we are |
| 31 | +| MUST | Harvard separation → code injection *grammatically* impossible | ✅ structural |
| 32 | +| MUST | Data language addition-only & Total (provably halting) | ✅ |
| 33 | +| MUST | Reversibility / Echo soundness — `reverse` gate on the *actual* grade; Lean proofs 0 `sorry/admit/axiom` | ✅ (carrier-aware + float-locals, ADR-0010) |
| 34 | +| MUST | ADR-0009 effect surface: Echo + Epistemic on declarations *and* function types | ✅ (#48–#50) |
| 35 | +| INTEND | First-class function *values* (lambdas) → activates the function-type effect check | ◻ next rung |
| 36 | +| INTEND | `gap-005`: value-level number-system semantics beyond `τ=int` | ◻ open |
| 37 | +| INTEND | `Settings → jtv` repo-slug rename (make the rebrand live) | ◻ manual |
| 38 | +| INTEND | PataCL Phase 1 → coprocessor implementation | ◻ external dep |
| 39 | +| WISH | v2 reversible-computing / quantum-algorithm simulation (Landauer, Grover/Shor) | ○ spec only |
| 40 | +| WISH | Router-visualization playground (the "killer demo") | ○ |
| 41 | +|=== |
| 42 | + |
| 43 | +== Absolute Zero |
| 44 | + |
| 45 | +Multi-prover formal verification of Certified Null Operations (CNO). ~65%, |
| 46 | +proof-completion phase. |
| 47 | + |
| 48 | +[cols="1,5,3",options="header"] |
| 49 | +|=== |
| 50 | +| Tier | Item | Where we are |
| 51 | +| MUST | Proofs green across provers: Coq 11/11 (0 `Admitted`), Lean 1631/1632, Agda `CNO.agda` clean | ✅ (2026-05-27) |
| 52 | +| MUST | Core CNO + category theory + statistical mechanics fully proven | ✅ |
| 53 | +| MUST | Trusted-base discipline — 72 Coq axioms triaged (52 trusted / 17 discharge / 3 property-test) | ◑ Phase 1 (PR #58) |
| 54 | +| MUST | No Python (RSR) | ⚠ currently violated (high blocker) |
| 55 | +| INTEND | v0.8 compliance sprint (40%); discharge 17 §a Coq backlog axioms; Phase-2 triage (Lean 52 + Idris2 7) | ◻ in progress |
| 56 | +| INTEND | Migrate Python→Rust; physics-constant dedup; v0.9 container verification | ◻ |
| 57 | +| WISH | v1.0 publication release + paper draft | ○ |
| 58 | +| WISH | Mizar (10% stub) + Isabelle (40%) brought to parity | ○ |
| 59 | +|=== |
| 60 | + |
| 61 | +== JanusKey |
| 62 | + |
| 63 | +Architecturally-reversible file operations (data loss "impossible" by design, not |
| 64 | +backups). ~60%; content-addressed (SHA256), Rust. |
| 65 | + |
| 66 | +[cols="1,5,3",options="header"] |
| 67 | +|=== |
| 68 | +| Tier | Item | Where we are |
| 69 | +| MUST | 100% reversible file ops by *architecture* | ◑ implemented — *formal proofs still pending* (per README) |
| 70 | +| MUST | Content-addressed (SHA256) storage, audit trail, transactions | ✅ |
| 71 | +| MUST | Coverage across p2p / e2e / aspect-security / concurrency | ✅ 56 tests / 64 points (CRG D→C blitz) |
| 72 | +| MUST | License = MPL-2.0 | ✅ migrated (a740439, #52); PMPL stragglers retired (#65) |
| 73 | +| INTEND | API stability review (stated current phase) | ◻ |
| 74 | +| INTEND | Land the formal reversibility proofs; climb CRG grade (D→C→…) | ◻ |
| 75 | +| WISH | Broader packaging / adoption | ○ thin in current state |
| 76 | +|=== |
| 77 | + |
| 78 | +== maa-framework — Mutually Assured Accountability |
| 79 | + |
| 80 | +The *Mutually Assured Accountability* framework. ⚠ *Not yet groundable from this |
| 81 | +session:* it is not in the current working repo scope, not cloned locally, and the |
| 82 | +repo-management tooling (`list_repos`/`add_repo`) was unavailable — so no MUST / |
| 83 | +INTEND / WISH rows are recorded here rather than invent them. Add it to scope |
| 84 | +(when the tooling is available) to populate this section from its own `STATE` and |
| 85 | +contractiles. |
| 86 | + |
| 87 | +== Where we are (synthesis) |
| 88 | + |
| 89 | +* *JtV* is the most mature and the only one advanced this session: core guarantees |
| 90 | + and the full Echo + Epistemic effect surface are done and proven; remaining work |
| 91 | + is feature-reach (function values) plus one manual rename. |
| 92 | +* *Absolute Zero* is deep in proof-completion — green across provers, grinding down |
| 93 | + axiom / Python debt toward a publishable v1.0. |
| 94 | +* *JanusKey* is feature- and test-complete in architecture but has not yet *proven* |
| 95 | + its headline reversibility claim; its license migration is now finished. |
| 96 | +* *maa-framework* awaits inclusion in working scope. |
0 commit comments