// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>

= Foundations Readiness Grades — Self-Assessment
:toc: auto
:status: Active
:date: 2026-05-28

FRG grades *languages*, not *specifications*. The FRG spec cannot
self-grade with an FRG letter, because the FRG spec is not a language.

What follows is therefore a *document-set self-assessment* — applying
FRG's internal-consistency criteria to the FRG document set itself, in
the same spirit as TRG's and ARG's `SELF-ASSESSMENT.adoc`.

== Current document-set status: COMPLETE-MINIMAL

*Assessed: 2026-05-28*

FRG v1.0 was just published. The document set is internally consistent
and structurally complete, but no language has yet been audited against
it.

== Document-set conformance

[cols="2,1,4", options="header"]
|===
| Conformance item | Status | Notes

| Normative spec exists in `.adoc`
| [OK]
| `FOUNDATIONS-READINESS-GRADES.adoc` (~22 KB, 12 sections)

| README.adoc
| [OK]
| `README.adoc`

| Self-assessment
| [OK]
| This document

| Machine-readable counterpart (`.a2ml`)
| [OK]
| `FOUNDATIONS-READINESS-GRADES.a2ml`

| Templates referenced from spec
| [OK]
| `templates/FRG-PROFILE-TEMPLATE.adoc`

| SPDX header on every file
| [OK]
| Verified at creation

| Inherits CRG/TRG/ARG vocabulary
| [OK]
| Grades X-A; release-stage mapping aligned; worst-of aggregation

| Inherits TRG qualifying-provers list
| [OK]
| `(inherited-from "TRG")` in a2ml; Idris2, Lean 4, Rocq, Agda

| Inherits TRG banned-constructs list
| [OK]
| `(inherited-from "TRG")` in a2ml verbatim

| Inherits TRG diversity-metrics
| [OK]
| Applied to peer-review and external-review criteria

| ARG-A requires FRG ≥ B cross-axis rule stated
| [OK]
| Spec §abstract; §1; §10; cross-axis block in a2ml

| Counterexample-driven regression formalised as a rung
| [OK]
| P3 in §3.2; §6.5 definition; ephapax `Counterexample.v` cited as canonical example

| Layered decomposition formalised as a rung
| [OK]
| P4 in §3.2; §6.4 definition; ephapax four-layer redesign cited as canonical example

| TypeLL 10-level lineage folded into evidence rungs
| [OK]
| L1-L10 in §3.4; grade-specific TypeLL floors at E (L2), D (L4), C (L6), B (L8), A (L10)

| VeriSimDB attestation integration specified
| [OK]
| §7; VCL-total proposition form; required from grade C

| Echidna integration specified
| [OK]
| §6.6; required from grade A; §4.7 evidence

| At least one language audited against FRG
| [No]
| Phase 4 of the framework rollout — ephapax (the canonical example
  for several rungs) is the most natural first audit target

| External review by language designers
| [No]
| Not yet — first audit cohort must complete before external review

| Adoption by any language outside hyperpolymath
| [No]
| Not yet — standard is brand new
|===

== Honest acknowledgments

* *The "≥ 3 qualifying provers" threshold at FRG-A is plucked from
  intuition.* It is the minimum number that breaks any single-prover
  ecosystem capture, but the exact number should be re-baselined
  against the first FRG-A candidate's actual cross-prover work.

* *The "100k differential tests per release" at A is order-of-
  magnitude.* The exact number should be re-baselined against the
  first FRG-A candidate's coverage.

* *The "kernel-soundness contribution within 12 months" at A is
  narrow.* It explicitly excludes mere bug-fix contributions and
  feature work — only soundness-relevant upstream contributions
  count. May be too narrow; re-baseline once tested.

* *The Echidna hard CI-gate at A* assumes Echidna remains the
  estate's neurosymbolic verifier of record. If a second neurosymbolic
  verifier emerges in the estate or upstream, this gate may relax to
  "any production neurosymbolic verifier with TRG ≥ B".

* *TypeLL = L10 hard gate at A* may be too strict for domain-specific
  languages whose semantics genuinely don't reach cross-cutting
  territory. A configuration language legitimately capping at L6
  should not be FRG-disqualified for failing L10; the per-language
  profile mechanism (§1.1 tightening) is the current workaround,
  but a future revision may relax the baseline.

* *FRG-F (provably-wrong unmarked) is novel.* No published
  language-grading standard the author is aware of has a "you
  *claim* you proved this but you didn't" rung. The grade exists
  because the failure mode is real (ephapax pre-redesign was in
  this position from at least 2026-03-28 until 2026-05-27). The
  evacuation path (mark archaeology + commit canonical redesign)
  is the discipline that got ephapax out of F.

* *The relationship to ARG-A is currently encoded as ARG-A requires
  FRG ≥ B.* This is a deliberate-but-debatable coupling. It excludes
  languages whose adoption is high but whose foundations lag (most
  historical production languages: Python, JavaScript, early Ruby).
  The coupling may tighten to FRG ≥ A once any single language has
  shown both can co-exist; or may loosen if it turns out unrealistic.

== Path forward

. Land per-language `spec/FRG-PROFILE.adoc` in affinescript, ephapax,
  my-lang following `templates/FRG-PROFILE-TEMPLATE.adoc`. Each at
  honest current grade. This is Phase 4 of the framework rollout.
. Extend `nextgen-languages/TOOLING-STATUS.adoc` with the FRG column
  alongside ARG / TRG / CRG / RSR. Update `language-status-tracker.jl`
  to surface FRG grades from each repo's profile.
. Once the first audit cohort lands, invite external review from
  formalisation-discipline practitioners outside hyperpolymath. The
  CompCert / CakeML / RustBelt / Idris2 communities are the natural
  reviewer pool.
. Adjust thresholds based on feedback before locking v1.0.
. After feedback cycle, FRG v1.0 becomes the load-bearing standard
  for language foundations claims in the estate.

== Standing rule

This self-assessment is itself a claim and is itself subject to the
invariant-path doc-claims grounder once it ingests the FRG directory.
Re-run after any change to this directory. If any file-path claim in
this document fails to ground, the self-assessment is invalid until
the gap is closed.
