Skip to content

foundations-readiness-grades

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History

foundations-readiness-grades

README.adoc

Foundations Readiness Grades (FRG)

Table of Contents

  • 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

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

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.