Finish the stale-fact sweep + add a language-registry consistency guard

.github/workflows/dogfood-gate.yml

@@ -257,14 +257,36 @@ jobs:
           echo "" >> "$GITHUB_STEP_SUMMARY"
           echo "Verifies that no language-implementation content (proofs, grammars, compilers, specs, or a re-vendored language directory) has leaked into the coordinator. Language code lives in each \`hyperpolymath/<lang>\` repo, referenced here — not embedded." >> "$GITHUB_STEP_SUMMARY"
 
+  # ---------------------------------------------------------------------------
+  # Job 5b: Language-registry consistency — every surface lists the same family
+  # ---------------------------------------------------------------------------
+  language-registry:
+    name: Language registry consistency
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      - name: Enforce language-registry consistency
+        run: bash hooks/validate-language-registry.sh
+
+      - name: Write summary
+        if: always()
+        run: |
+          echo "## Language Registry Consistency" >> "$GITHUB_STEP_SUMMARY"
+          echo "" >> "$GITHUB_STEP_SUMMARY"
+          echo "Verifies every language appears on all registry surfaces (\`languages/\`, \`LANGUAGES.a2ml\`, the boundary-hook \`LANGS\` list, \`ECOSYSTEM.a2ml\`, and the status tracker), so the family cannot silently drift out of sync. Canonical set: \`languages/*.md\`." >> "$GITHUB_STEP_SUMMARY"
+
   # ---------------------------------------------------------------------------
   # Job 6: Dogfooding summary
   # ---------------------------------------------------------------------------
   dogfood-summary:
     name: Dogfooding compliance summary
     runs-on: ubuntu-latest
     timeout-minutes: 15
-    needs: [a2ml-validate, k9-validate, empty-lint, groove-check, coordinator-boundary]
+    needs: [a2ml-validate, k9-validate, empty-lint, groove-check, coordinator-boundary, language-registry]
     if: always()
 
     steps:

EXPLAINME.adoc

@@ -22,20 +22,21 @@ NOTE: `tentacles-agentic-syllabus` is NOT a programming language. It is an
 educational framework using My-Lang's dialects as a curriculum vehicle. Never
 audit it as a language implementation.
 
-== Claim 1: "Ten languages that cover the full spectrum of modern software challenges"
+== Claim 1: "A family of languages covering the full spectrum of modern software challenges"
 
 [quote, README]
 ____
-A coordinated effort to design and develop ten programming languages that
+A coordinated effort to design and develop a family of programming languages that
 collectively cover the full spectrum of modern software challenges, from
 AI-native development to formally verified real-time systems.
 ____
 
 === How it works
 
-The eight core languages plus two specialised languages are designed to
-complement each other, not compete. They occupy distinct cells in the design
-space (each maintained as a standalone `hyperpolymath/<lang>` repo):
+The family currently spans fourteen languages plus the KitchenSpeak DSL — the canonical
+list is `.machine_readable/LANGUAGES.a2ml`. They are designed to complement each other, not
+compete, each occupying a distinct cell in the design space (each maintained as a standalone
+`hyperpolymath/<lang>` repo). The table below shows the representative core:
 
 [cols="1,1,2,1"]
 |===
@@ -90,9 +91,14 @@ Gossamer backend. Rust compiler, Coq proofs.
 | Rust (17 crates), Coq proofs
 |===
 
+NOTE: The table shows a representative core. The full family also includes *betlang*
+(probabilistic), *JtV* (systems / Harvard architecture), *Haec* (trope-particularity),
+*error-lang* (pedagogical), *Tangle* (topological), and *007* (a private agent
+meta-language) — see `.machine_readable/LANGUAGES.a2ml` for the canonical registry.
+
 NOTE: *KitchenSpeak* — an experimental applied-type-theory teaching DSL
 (seven-type kitchen orchestration: Tropical, Linear, Choreographic, Echo,
-Dyadic, Ceremonial, Primitive) — is NOT one of the ten core languages and is
+Dyadic, Ceremonial, Primitive) — is NOT one of the core languages above and is
 no longer carried in this repo. It is canonical at the standalone
 link:https://github.com/hyperpolymath/kitchenspeak[`hyperpolymath/kitchenspeak`]
 repository (v2.0: physics-in-the-types, reference OCaml compiler, machine-checked

PROOF-NEEDS.md

@@ -6,10 +6,14 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 ## Current State
 
-- **src/abi/*.idr**: YES (in oblibeny) — `Interface.idr`
-- **Dangerous patterns**: 4 `Admitted` in ephapax/formal/Semantics.v (ctx_transfer 15/24, subst_lemma, preservation)
-- **LOC**: ~456,000 (OCaml + Rust + Coq + Idris2 + Lean)
-- **Existing proofs**: Ephapax has Coq proofs, Tangle has Lean proofs, Idris2 in multiple sub-languages
+`nextgen-languages` is a pure coordinator and holds **no** proof code. This file tracks the
+family's proof gaps across the standalone `hyperpolymath/<lang>` repos; every path below is
+relative to the named language's own repo, not this one.
+
+- **Ephapax** — Coq proofs present; 4 `Admitted` remain in `formal/Semantics.v` (ctx_transfer 15/24, subst_lemma, preservation, + one more).
+- **Tangle** — Lean proofs present (`Tangle.lean`); coverage partial.
+- **Oblíbený** — Idris2 ABI present (`src/abi/Interface.idr`); minimal.
+- **AffineScript** — OCaml type checker + Rust runtime; soundness proofs outstanding.
 
 ## What Needs Proving
 

README.adoc

@@ -43,9 +43,9 @@ Status: design-stage, with partial specifications and experimental implementatio
 
 ---
 
-=== KRL — Knot Resolution Language (Tangle)
+=== Tangle
 
-A topologically inspired language where programs are represented as tangles (braids), and equivalence is defined by isotopy.
+A topologically inspired language where programs are represented as tangles (braids), and equivalence is defined by isotopy. Its IR (TangleIR) is consumed by the separate *KRL resolution stack* (`krl → TangleIR → VeriSimCore → Skein.jl / QuandleDB`), which is tracked by the database estate — not part of this coordinator's language family.
 
 * Composition and tensor operations correspond to braid structure
 * Formal semantics specified
@@ -141,7 +141,7 @@ Type-theoretic boundaries are made explicit: total proof-like fragments are dist
 
 These languages are designed to work with systems that treat equivalence, provenance, and semantic identity as first-class concepts:
 
-KRL ↔ QuandleDB / Skein
+Tangle (via the separate KRL resolution stack) ↔ QuandleDB / Skein
 JtV ↔ future equivalence-aware runtime and storage models
 
 See the nextgen-databases repository for details.
@@ -196,7 +196,7 @@ production system. The work it tracks spans, across the individual language repo
 Each language lives in its own `hyperpolymath/<lang>` repo; start there. For orientation:
 
 * link:https://github.com/hyperpolymath/tangle[`hyperpolymath/tangle`] — `Tangle.lean`, the
-  mechanised type-safety proof for the Tangle (KRL) core; topological language design
+  mechanised type-safety proof for the Tangle core; topological language design
 * link:https://github.com/hyperpolymath/jtv[`hyperpolymath/jtv`] — computation as
   path-based construction
 

hooks/validate-language-registry.sh

@@ -0,0 +1,107 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Language-registry consistency guard.
+#
+# nextgen-languages registers its language family across several surfaces. They
+# drifted badly before (a language present on one surface, missing on another),
+# so this check fails the build when they disagree.
+#
+# Source of truth: the human-facing pointers in `languages/<id>.md`. Every other
+# surface MUST list exactly that same set of ids:
+#   - .machine_readable/LANGUAGES.a2ml   ([[language]] stanzas; forward-looking entries with
+#                                         status "proposed"/"exploratory" are exempt — they
+#                                         are not yet committed and carry no languages/ pointer)
+#   - hooks/validate-coordinator-boundary.sh   (the LANGS re-vendoring guard list)
+#   - .machine_readable/6a2/ECOSYSTEM.a2ml     ([language-repos] keys)
+#   - language-status-tracker.jl               (const LANGUAGES — must be a SUPERSET;
+#                                               it also tracks playgrounds/ecosystem/umbrella)
+#
+# See 0-AI-MANIFEST.a2ml and EXTRACTION-MANIFEST.md.
+set -euo pipefail
+
+cd "$(git rev-parse --show-toplevel)"
+
+ERRORS=0
+
+# ── Source of truth: languages/<id>.md pointers (excluding README) ────────────
+family() {
+  for f in languages/*.md; do
+    b="$(basename "$f" .md)"
+    [[ "$b" == "README" ]] || printf '%s\n' "$b"
+  done | sort -u
+}
+
+# ── LANGUAGES.a2ml: committed [[language]] ids (status not proposed/exploratory) ──
+a2ml_registered() {
+  awk '
+    /^\[\[language\]\]/ { if (id != "") print id, status; id=""; status="" ; next }
+    /^id[ \t]*=/       { line=$0; sub(/^id[ \t]*=[ \t]*"/,"",line); sub(/".*/,"",line); id=line }
+    /^status[ \t]*=/   { line=$0; sub(/^status[ \t]*=[ \t]*"/,"",line); sub(/".*/,"",line); status=line }
+    END { if (id != "") print id, status }
+  ' .machine_readable/LANGUAGES.a2ml \
+    | awk '$2 != "proposed" && $2 != "exploratory" { print $1 }' | sort -u
+}
+
+# ── boundary-hook LANGS list ──────────────────────────────────────────────────
+hook_langs() {
+  grep -E '^LANGS=' hooks/validate-coordinator-boundary.sh \
+    | sed -E 's/^LANGS="//; s/"[[:space:]]*$//' \
+    | tr ' ' '\n' | sed '/^$/d' | sort -u
+}
+
+# ── ECOSYSTEM.a2ml [language-repos] keys (excluding the `note` key) ───────────
+ecosystem_keys() {
+  awk '
+    /^\[language-repos\]/ { inblk=1; next }
+    /^\[/                 { inblk=0 }
+    inblk && /^[^#].*=/ {
+      key=$0; sub(/[ \t]*=.*/,"",key); gsub(/["[:space:]]/,"",key)
+      if (key != "note" && key != "") print key
+    }
+  ' .machine_readable/6a2/ECOSYSTEM.a2ml | sort -u
+}
+
+# ── tracker const LANGUAGES vector (quoted ids) ───────────────────────────────
+tracker_langs() {
+  awk '/const LANGUAGES[ \t]*=[ \t]*\[/ { inblk=1; next } inblk && /^\]/ { inblk=0 } inblk' \
+    language-status-tracker.jl \
+    | grep -oE '"[^"]+"' | tr -d '"' | sort -u
+}
+
+FAMILY="$(family)"
+COUNT="$(printf '%s\n' "$FAMILY" | wc -l | tr -d ' ')"
+printf 'language-registry: source of truth = languages/*.md (%s entries)\n' "$COUNT"
+
+# report_diff <surface-name> <surface-set> <mode: exact|superset>
+report_diff() {
+  local name="$1" have="$2" mode="$3" missing extra
+  missing="$(comm -23 <(printf '%s\n' "$FAMILY") <(printf '%s\n' "$have") || true)"
+  if [[ -n "$missing" ]]; then
+    printf 'ERROR: %s is MISSING family languages:\n' "$name"
+    printf '%s\n' "$missing" | sed 's/^/  - /'
+    ERRORS=$((ERRORS + 1))
+  fi
+  if [[ "$mode" == "exact" ]]; then
+    extra="$(comm -13 <(printf '%s\n' "$FAMILY") <(printf '%s\n' "$have") || true)"
+    if [[ -n "$extra" ]]; then
+      printf 'ERROR: %s lists languages NOT in languages/ (add a pointer, or remove them):\n' "$name"
+      printf '%s\n' "$extra" | sed 's/^/  - /'
+      ERRORS=$((ERRORS + 1))
+    fi
+  fi
+}
+
+report_diff ".machine_readable/LANGUAGES.a2ml"             "$(a2ml_registered)" exact
+report_diff "hooks/validate-coordinator-boundary.sh LANGS" "$(hook_langs)"      exact
+report_diff ".machine_readable/6a2/ECOSYSTEM.a2ml"         "$(ecosystem_keys)"  exact
+report_diff "language-status-tracker.jl const LANGUAGES"   "$(tracker_langs)"   superset
+
+if [[ "$ERRORS" -gt 0 ]]; then
+  printf '\nlanguage-registry check FAILED (%s surface(s) out of sync).\n' "$ERRORS"
+  printf 'Every language must appear on all registry surfaces. Update them together —\n'
+  printf 'the canonical set is languages/*.md; see .machine_readable/LANGUAGES.a2ml.\n'
+  exit 1
+fi
+
+printf 'language-registry: OK (all surfaces agree on the %s-language family)\n' "$COUNT"
+exit 0

language-status-tracker.jl

@@ -5,7 +5,7 @@
 
 using Dates
 
-const REPOS_DIR = joinpath(homedir(), "Documents/hyperpolymath-repos")
+const REPOS_DIR = get(ENV, "HYPERPOLYMATH_REPOS_DIR", joinpath(homedir(), "Documents/hyperpolymath-repos"))
 
 # All known language repos
 const LANGUAGES = [