Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
305 lines (258 loc) · 16.6 KB

AFFIRMATION.adoc

File metadata and controls

305 lines (258 loc) · 16.6 KB
Raw

AFFIRMATION — nextgen-typing, as of 2026-06-16

the No-Bullshit file: what we affirm was true and checkable at this moment

Note

Genre. An affirmation is a solemn declaration of the truth of a statement, made by someone who declines to swear an oath. That is exactly what this is: our truth-as-best-believed at a stamped instant — binding on our honesty, not a claim of infallibility. It is not the README and not the EXPLAINME:

File Answers Tense

README.adoc

Where is this going, and why? — the pipeline overview and steering

future / aspirational

EXPLAINME.adoc

How is it built, and what’s the evidence? — the coordination mechanism

descriptive / mechanism

AFFIRMATION.adoc (this file)

What can we honestly affirm was true and checkable at a stamped moment?

a frozen instant, falsifiable

nextgen-typing is a coordination monorepo, not a compiler or a proof project. The affirmation that matters here is about the coordination layer itself: that its registry and cross-file invariants build and are internally consistent, and that it holds no proofs of its own — by design.
Table of Contents

What this is, and how it is designed to work

What it is. A short, dated, jointly-signed snapshot of what we can honestly and verifiably claim about this repo at one exact commit. Nothing here is marketing (that is the README) and nothing is engineering evidence for a constituent repo’s compiler or proofs (those claims belong in those repos). This file is the receipt for the coordination layer.

How it is designed to work. Three moving parts make it trustworthy:

  1. Ground truth, not memory. Every claim below was produced by running the tool in the session that wrote this file (the pipeline-drift guard, the must/trust gates, the template-residue check, and the proof-checker harness this repo ships). Where a status doc said otherwise, the live run wins and we flag the contradiction.

  2. A frozen anchor. The file names the exact commit SHA, branch, UTC timestamp, and toolchain (see Verifiable anchor), so "true" always means "true at this point". Move the SHA and this file becomes a draft until re-run.

  3. A real signature. It is landed by a signed git commit; that signature over this content at the anchored SHA is what makes the affirmation tamper-evident and attributable — not the prose alone.

We are fallible. We can be wrong, stale, or simply mistaken about our own work. This file is our best honest belief, not a proof of its own correctness. Treat it as a falsifiable claim, not gospel.

The epistemic contract (read this before you trust or attack)

This document records our best joint belief at the timestamp below. It is not a guarantee of correctness. We may be wrong. We may have missed something — a drifted doc, a stale registry line, a public description that overruns the tree.

No intentional overclaim. That is the only guarantee here: we have not knowingly inflated anything. This repo makes no compiler-correctness, proof-soundness, or benchmark claim, and this file does not invent one. Where a checker passed, we say "passed". Where one failed, we say "failed" and why. Where the in-tree proof files are unconfigured RSR template residue, we say so plainly. If you find an honest claim here that turns out false, that is an error to be fixed — not a lie.

Standing invitation to refute. You are invited to bulldoze any claim in this file. We want that. But the fair form of the attack is:

  1. Read this file at the stamped commit.

  2. Reproduce (or fail to reproduce) the checks in Reproduce it yourself.

  3. Then tell us where the discrepancy is, against the artefact as it stood at this moment — so we can either justify it or concede it on the record.

An attack that skips steps 1–2 is attacking a strawman of a different date.

No fights before the facts are cleared up. We are not interested in a dispute over a claim until the discrepancy has actually been checked against the artefact at this commit and we have had the chance to either justify it or concede it on the record. Good faith both ways: bring a reproducible discrepancy and we will fix the claim, the doc, or the registry — promptly and without defensiveness. The goal is a corrected record, not a won argument.

Verifiable anchor

Repo

hyperpolymath/nextgen-typing (the type-theory pipeline coordination monorepo — contains no compiler code)

Branch

main

Commit (HEAD)

e9897daf4ba1d2104f78abd5f660a870279eda5b

Permalink

https://github.com/hyperpolymath/nextgen-typing/tree/e9897daf4ba1d2104f78abd5f660a870279eda5b

Verified (UTC)

2026-06-16T12:28:36Z

Working-tree delta at verification

Clean (git status --porcelain empty) at the moment the checks below were run. This AFFIRMATION file is then added as a new untracked file; it does not change any check result above it. The results recorded here are HEAD as-is.

Toolchain

just 1.50.0 · bash 5.2.21 · git 2.43.0 · Idris2 0.8.0 · Lean 4.13.0 · Agda 2.8.0 · Coq 8.18.0 · TLA+ tlc not installed

HEAD commit signature

GPG-signed (RSA 9639451754496E51D6B537CAD119017EBF695AB1, "hyperpolymath", j.d.a.jewell@open.ac.uk) — "Good signature" reported by git log --show-signature.
Important
 If you are reading this at a later commit, the claims may have drifted. Re-run Reproduce it yourself and write a fresh affirmation; do not trust a stale one.

Companion documents and repo metadata (cross-check)

This affirmation should be read against the repo’s own public claims. Where they drift from what we verified, we say so here rather than quietly leave the reader to find out.

  • README.adoc — present. "nextgen-typing — The Hyperpolymath Type Theory Pipeline". States plainly: "It does not contain compiler code." Verified consistent with the tree.

  • EXPLAINME.adoc — present. EXPLAINME.adoc. Explicitly: "This repo makes no claims about compiler correctness, proof soundness, or benchmark results." Verified consistent with what we ran.

  • 0-AI-MANIFEST.a2ml — present. The repo’s read-first invariant file; invariant #3 is "No compiler claims here". This AFFIRMATION upholds that invariant rather than breaching it.

  • GitHub repo description (fetched in-session via gh repo view) — "Coordination monorepo for the Hyperpolymath type-theory pipeline — Kategoria/Katagoria, TypeLL, typed-Wasm, PanLL, and minimal calibration calculi such as TypeFix Zero." Drift: the strings "Kategoria", "TypeFix Zero", and "calibration calculi" do not appear anywhere in the tree at this commit (the README’s main chain spells it "katagoria", which it also flags as not yet created). The description is ahead of the artefact; treat it as steering, not a tree claim.

  • GitHub topics — dependent-types, formal-methods, linear-types, partiality, turing-completeness, type-theory, typed-wasm, universe-hierarchy. Caveat: these describe the pipeline this repo coordinates, not artefacts in this repo. None of partiality, turing-completeness, or universe-hierarchy corresponds to any proved-here content — they are properties of the constituent repos (typell / typed-wasm / tropical-resource-typing), not of this coordination layer.

The honest state (one breath)

nextgen-typing is a documentation-and-registry coordination layer for the katagoria → typell → typed-wasm → PanLL pipeline. Its job is to keep the cross-repo story consistent, and at this commit that job is being done: the pipeline-drift guard and the must/trust correctness gates pass green. It holds no proofs of its own — the proof directory is unconfigured RSR-template residue that does not compile as shipped, and every real proof obligation lives in the constituent repos, exactly as the manifest says it should.

What is solid (and how we checked)

  • The pipeline-drift registry guard passes — verified green this moment. just validate-pipeline-drift → scripts/check-pipeline-drift.sh exits 0, with every check PASS: all six canonical files present (README.adoc, docs/ARCHITECTURE.adoc, docs/PIPELINE.adoc, and the three .machine_readable/6a2/ A2ML files); the canonical chain katagoria → typell → typed-wasm → PanLL matches exactly across README, ARCHITECTURE, PIPELINE, STATE and ECOSYSTEM; the "open-ended TypeLL" framing is consistent across README/ARCHITECTURE/PIPELINE/META; katagoria marked Active consistently; dates synchronized (all read 2026-04-12); and no stale status phrases. This is the core "is the coordination internally consistent?" check, and it is green.

  • The "must" correctness gate passes. just must-check exits 0: LICENSE present, README present, no banned Dockerfile/Makefile, and SPDX-header presence on source files.

  • Licence is MPL-2.0, internally consistent. just trust-license-content passes; the in-tree LICENSE is the Mozilla Public License Version 2.0 and in-tree source/doc files carry SPDX-License-Identifier: CC-BY-SA-4.0. (Note: the trust-verify aggregate recipe fails — see loud-failures — but that is a Containerfile-pinning rule, not a licence problem.)

  • No secrets committed. just trust-no-secrets-committed passes (no .env, credentials.json, or .env.local).

  • The Coq template proof, taken alone, compiles. just proof-check-coq exits 0 (coqc verification/proofs/coq/TypeSafety.v → exit 0). But read the nuance below before reading anything into this: it proves a toy expression-language type_soundness theorem labelled "Template — replace with your project’s type system", not any nextgen-typing claim.

The honest nuance you must not lose (proved-CORE vs unproved-IMPLEMENTATION)

This repo proves nothing about the typing pipeline, and that is correct by design. The distinction here is sharper than the usual "proved core vs tested implementation":

  • The verification/proofs/ tree (idris2/, lean4/, agda/, coq/, tlaplus/) is unconfigured RSR template residue. The files say so in their own headers — e.g. verification/proofs/idris2/Types.idr line 5: "Template — replace with your project’s core types." They prove generic example lemmas (a bounded-Nat, a toy expression language), not pipeline properties.

  • PROOF-STATUS.md reports 0% proven (0 of 7 obligations) — and the live run confirms this rather than contradicting it: there is no nextgen-typing proof to run.

  • The genuine proof obligations for this pipeline live in the constituent repos (typell, typed-wasm, tropical-resource-typing, katagoria), and this coordination layer makes no claim to have discharged them. Anyone reading the presence of .idr/.lean/.agda/.v files here as "nextgen-typing has formal proofs" is overclaiming on the repo’s behalf.

Known-incomplete but honestly fenced (loud failures, never silent)

These three checks fail loudly at this commit. They are real findings, fenced here so no reader mistakes them for green:

  • just proof-check-idris2 FAILS (exit 1). The Idris2 template proofs do not even compile as shipped: Module name Types does not match file name "verification/proofs/idris2/Types.idr" (and the same module-vs-path mismatch for every ABI/.idr). So the Idris2 "proofs" prove *nothing right now — a loud, visible failure, not a silent pass. (proof-check-all therefore also surfaces these failures.)

  • just proof-scan-dangerous FAILS (exit 1) — but on false positives. It flags 8 files for "dangerous patterns", yet every hit is the warning comment itself (e.g. the line "All proofs MUST be constructive (no believe_me, no assert_total)" trips the believe_me/assert_total matcher). There is no actual believe_me, sorry, Admitted, or postulate in proof position — the scanner is matching its own documentation. A scanner bug, recorded as such; not evidence of unsound proofs (there are no load-bearing proofs to be unsound).

  • just verify-template FAILS (exit 1). Unreplaced {{PLACEHOLDER}} template tokens remain in QUICKSTART-MAINTAINER.adoc, QUICKSTART-DEV.adoc, READINESS.md, TEST-NEEDS.md, TEMPLATE-STANDARDS-AUDIT.adoc, and container/compose.toml; the Justfile still references rsr-template-repo; and the Groove manifest still has port 0. This repo is a partly-uninstantiated RSR template — honest, visible debt.

  • just trust-verify FAILS (exit 1) at trust-container-images-pinned: the Containerfile base images are not digest-pinned (@sha256:). A supply-chain hygiene gap, not a coordination-correctness problem.

Outstanding / weak / refuted (no spin)

  • Public GitHub description over-runs the tree (drift). It advertises "Kategoria/Katagoria … TypeFix Zero … minimal calibration calculi", none of which exist in the repo at this commit. Not refuted-as-false-claim (it is steering text), but flagged so the reader is not misled.

  • katagoria is declared "✅ Active" in the README table yet the manifest (invariant #4) and EXPLAINME both say it "does not exist yet / not yet created". Internal tension between the status glyph and the prose; the honest reading is "planned, not created".

  • No nextgen-typing-specific proof exists — by design, but stated plainly so no one infers otherwise from the populated verification/proofs/ tree.

  • TLA+ cannot be checked in this environment (tlc not installed), so verification/proofs/tlaplus/StateMachine.tla was not exercised at all.

Reproduce it yourself

From the repo root, at the commit above:

git rev-parse HEAD                  # expect e9897daf4ba1d2104f78abd5f660a870279eda5b
git status --porcelain              # expect empty (clean) before adding this file

just validate-pipeline-drift        # expect exit 0 — "PASS: no pipeline drift detected."
just must-check                     # expect exit 0 — "All must checks passed"
just proof-check-coq                # expect exit 0 — toy TEMPLATE proof compiles (not a pipeline claim)

# The loud failures (expected to FAIL — that is the honest state, not a regression):
just proof-check-idris2             # expect exit 1 — module-name vs file-path mismatch in template .idr files
just proof-scan-dangerous           # expect exit 1 — false positives on the warning COMMENTS, no real dangerous tactics
just verify-template                # expect exit 1 — unreplaced {{PLACEHOLDER}} tokens + rsr-template-repo refs
just trust-verify                   # expect exit 1 — Containerfile base images not @sha256-pinned

To confirm the no-proofs-here invariant directly: the files under verification/proofs/ self-identify as templates (grep -n Template verification/proofs/idris2/Types.idr), and PROOF-STATUS.md reports 0% proven (0 of 7).

One-line characterisation (quote this)

"A type-theory pipeline coordination monorepo whose registry/docs consistency guard (validate-pipeline-drift) and must/licence gates pass green this moment, that holds no proofs of its own — the in-tree proof tree is unconfigured RSR template residue that does not compile, and all real proof obligations live in the constituent repos — with honest, loudly-failing template-instantiation debt (verify-template, Idris2 module paths, Containerfile pinning) still on the queue. A coordination layer, not a verified artefact. No intentional overclaim."

Joint attestation

We, the undersigned, assert that to the best of our joint belief at the timestamp above, every claim in this file is true and was checked as described — with no intentional overclaim, and with the open gaps stated rather than hidden.

  • Engineering party (AI): Claude Opus 4.8 (claude-opus-4-8[1m]) — ran the build/test/proof checks recorded here on 2026-06-16T12:28:36Z and stands behind this wording as a faithful report of those runs.

  • Owner / maintainer: Jonathan D.A. Jewell — signs by committing this file with -S (id_ed25519_signing); the git commit signature over this content, at the commit SHA recorded above, is the cryptographic form of this affirmation.

    Signed-off-date: (fill on signing)

Tip
 The authoritative, tamper-evident signature is the signed git commit that lands this file. If the SHA in Verifiable anchor matches the parent of that commit and the commit verifies, this affirmation is anchored. If they don’t match, treat the file as a draft.