// 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 (FRG)
:toc:

* *Status:* Active, v1.0, 2026-05-28
* *License:* PMPL-1.0-or-later (MPL-2.0 automatic legal fallback)
* *Companion to:* Toolchain Readiness Grades (TRG) v1.0, Adoption Readiness Grades (ARG) v1.0, Component Readiness Grades (CRG) v2.2
* *Part of:* Rhodium Standard Repositories (RSR)

== What this is

FRG grades the *language as a mathematical artefact*. It sits at the
language-whole tier of the estate grading hierarchy:

* *CRG* grades individual *components*.
* *TRG* grades the *toolchain*.
* *ARG* grades the language as a *thing someone can adopt*.
* *FRG* grades the language's *mathematical foundations*.

FRG uses the same letter grades as CRG, TRG, and ARG
(`X | F | E | D | C | B | A`) and the same worst-of-any-required-element
aggregation rule. The evidence required at each grade asks a different
question: *"is the typing discipline mathematically grounded?"*

== Why it exists

Three reasons:

1. CRG grades components, TRG grades the toolchain, ARG grades
   adoption — none of those answer *"is the language's typing
   discipline mathematically sound?"*. That question belongs at the
   language-whole tier.
2. The hyperpolymath estate has 17+ languages, several of which carry
   strong soundness claims (affinescript's QTT-affine fragment,
   ephapax's dyadic modality, vcl-ut's 10-level type-safety lineage,
   typed-wasm's verifier-as-spec). FRG provides a uniform yardstick
   for comparing them on the foundations axis.
3. The existing `PROOF-NEEDS.md` and `PROOF-STATUS.a2ml` per-repo
   conventions are good catalogs of what's missing but have no
   *rubric* for grading the overall mathematical maturity. FRG
   provides that rubric.

== Files in this directory

[cols="1,3", options="header"]
|===
| File | Purpose

| `FOUNDATIONS-READINESS-GRADES.adoc`
| The normative spec. Read this first.

| `README.adoc`
| This file.

| `FOUNDATIONS-READINESS-GRADES.a2ml`
| Machine-readable counterpart of the spec.

| `SELF-ASSESSMENT.adoc`
| FRG applied to itself (insofar as that's meaningful — FRG grades
  languages, not specs; the doc set is self-assessed against
  internal-consistency).

| `templates/FRG-PROFILE-TEMPLATE.adoc`
| The per-language profile template referenced from §1.1 of the spec.
  Each adopting language publishes `spec/FRG-PROFILE.adoc` in its repo
  following this template.
|===

== Quick mental model

[cols="^1,4", options="header"]
|===
| Grade | Meaning

| X | No formal artifact. Honest position for most new languages.
| F | Provably wrong formalisation that has not been marked as archaeology. Rare and important — see §4.2 of the spec.
| E | Well-formedness only: syntax + typing judgment formalised in a qualifying prover; no preservation claim yet.
| D | Preservation theorem *stated*; admits explicitly tracked; honest about what's open.
| C | Preservation *closed*: 0 admits, 0 axioms, 0 sorries, 0 banned constructs.
| B | Layered decomposition + cross-prover replication (≥ 2 provers); counterexample regression suite.
| A | Cross-prover ≥ 3 + Echidna in CI + 100k-test differential testing + kernel-soundness contribution upstream.
|===

== Demotion is immediate

Loss of any A-grade gate — kernel-soundness contribution lapses past
12 months, Echidna gate disabled, cross-prover falls below 3, banned
construct introduced anywhere in the proof tree — *immediately*
demotes the language. There is no grace period. Same rule as TRG §5.8
and ARG §4.8.

A single new `Admitted` / `sorry` introduced into the proof tree is
sufficient to demote from C, B, or A to the next-lower grade whose
evidence still holds.

== How strict is this really?

See spec §11. Honest answer: FRG-A is calibrated against CompCert /
CakeML — end-to-end verified compilers with cross-prover replication
and kernel-soundness contributions upstream. The author expects:

* ~1 hyperpolymath language to reach FRG-C in year one (ephapax,
  post-four-layer-redesign).
* ~0 to reach FRG-B in year one.
* ~0 to reach FRG-A in year one.

That is the correct order of magnitude. If FRG-A becomes easy to hit,
the bar is wrong and the standard MUST be raised.

== Per-language profiles

FRG is the baseline. Each hyperpolymath language is expected to
publish a `spec/FRG-PROFILE.adoc` in its own repo that tightens FRG
with language-specific obligations. A profile may only tighten, never
loosen. See spec §1.1 and `templates/FRG-PROFILE-TEMPLATE.adoc`.

== Interaction with the other graders

* *vs. CRG:* CRG grades components inside the language project (a
  parser, a formatter, a stdlib module). FRG grades the language's
  mathematical foundations as a whole. Where CRG and FRG would both
  apply (e.g. a formalisation directory is itself a component), both
  grades are published independently. FRG ≤ worst-of(CRG over all
  required formalisation components).
* *vs. TRG:* TRG grades the toolchain. FRG grades the calculus that
  the toolchain implements. The two are independent — a language can
  be FRG-C (preservation closed) and TRG-D (toolchain incomplete),
  or vice versa. The only coupling is via the `qualifying-provers`
  and `banned-constructs` lists, both inherited verbatim from TRG.
* *vs. ARG:* FRG and ARG are independent except for one coupling:
  *ARG-A requires FRG ≥ B*. This excludes school-grade adoption
  claims for languages whose foundations have not yet entered
  layered / cross-prover territory.
* *vs. RSR:* RSR grades repository hygiene. FRG-graded language repos
  MUST be RSR-compliant at the level required by TRG at the same
  grade.

== Open invitation

If you think FRG is too lax (or too strict in a way that lets bad
work hide), file an issue with concrete evidence and a proposed
tightening. FRG earns trust by surviving critique.

Particular invitations:

* Specify a *fifth* qualifying prover that should join {Idris2, Lean
  4, Rocq, Agda}, with evidence of soundness pedigree.
* Specify an alternative neurosymbolic verifier that could relax the
  Echidna coupling at FRG-A.
* Argue that the "kernel-soundness contribution within 12 months"
  gate at A is wrong — too narrow, too broad, wrong cadence.
