Rocq (9.0)

This assessment applies the coupling account — coupling as access to a shared resource, and the coupling floor [1], [2] — and the knowledge-embodiment theorem [3]; the language is assessed against its official reference [4].

1 Assessment

This page assesses Rocq in five parts: core coupling — what the language’s own constructs force; ecosystem coupling — what the surrounding platform, tooling, and community cost; engineering readiness — whether the artifact can be reproduced, verified, observed, worked in quickly, connected to other languages, and governed openly; the profile — the unscored facts a score cannot express; and the scoring detail — the mechanism marks and the arithmetic behind every score. A ✅ bullet marks a construct that helps. A ⚠️ or ❌ bullet marks a cost; the scoring model does not price every cost named here.

Core coupling 85/100 · Ecosystem coupling 69/100 · Engineering readiness 49/100

1.1 Core coupling

1.1.1 Type

  • ✅ Dependent types decouple a specification from its implementation: A type may mention a value, so a sorted list or a length-indexed vector is a type and a term of that type is the proof that the specification holds
  • ✅ The Curry–Howard correspondence equates propositions with types: A proposition is a type and a proof is a program, so logic and computation are written in one language
  • ✅ Inductive types define the data and the proofs over it together: An Inductive declaration fixes the constructors, and recursion over them is checked for coverage
  • ✅ The universe hierarchy stratifies types: Prop holds propositions, Set holds program data, and Type holds types, so a type cannot contain itself
  • ✅ Type classes and records express an interface: A Class or a Record states a structure and instance resolution selects the implementation, so reuse does not require inheritance
  • ⚠️ Definitional equality is the checker’s equality: Two terms that are equal only up to a lemma are not interchangeable without a rewrite, so an implementation must be shaped to compute the way the checker reduces

1.1.2 Construction

  • ✅ The logic core is pure: A Gallina term has no side effect, so building a value cannot change shared state
  • ✅ The tactic language is separate from the term it builds: A proof script constructs a Gallina term, and the kernel checks that term, so the proof strategy and the proof object are distinct artifacts
  • ✅ Definitions are checked terms: Definition and Fixpoint each name a term that the kernel type-checks before it is used
  • ✅ Modules and functors confine names: A Module Type states a signature and a Module implements it, so a name is reachable only through its path
  • ✅ Extraction separates verified construction from the runtime: Extraction emits OCaml, Haskell, or Scheme, so verification is decoupled from the implementation language
  • ⚠️ Totality is required: Every Fixpoint must be shown to terminate, so a construction that is correct but not obviously decreasing needs a measure or a well-founded relation

1.1.3 Memory

  • ✅ The logic core names no memory: A Gallina term has no address, no allocation, and no free operation, so a proof cannot couple to a memory layout
  • ✅ Collection belongs to the runtime: The checker is an OCaml program with its own collector, and the extracted program uses its target language’s collector
  • ✅ Reduction strategy is a tactic choice: cbn, cbv, lazy, vm_compute, and native_compute select how a term is reduced, so checking cost is stated where it is needed
  • ⚠️ A large reduction consumes memory without a visible allocation: A vm_compute or native_compute over a large term can exhaust memory while the source names no allocation
  • ⚠️ native_compute compiles a module through OCaml: It evaluates the term through code the OCaml compiler produced at proof time, trading the kernel’s own reduction for speed

1.1.4 Error

  • ✅ A wrong proof is a type error: A term that does not inhabit the goal is rejected when it is checked, before any extracted code runs
  • ✅ Tactic failure is a structured signal: Ltac combinators such as try, repeat, first, and progress branch on success and failure, so a tactic script has a recovery path
  • ✅ Fail asserts that a command is rejected: A development can test that a wrong proof fails, which keeps a tactic honest
  • ✅ Qed runs the kernel check and Defined records the term: The sealing decision is explicit at the end of a proof
  • ⚠️ Admitted and admit leave a gap the checker accepts: A development can be declared complete with an unproved lemma, so the guarantee holds only if the development contains none
  • ⚠️ Axiom, Parameter, and Hypothesis add an assumption without a proof: The soundness of a result is relative to the axiom set it used

1.1.5 Concurrency

  • ✅ The logic core is sequential: A Gallina term is a pure value, so there is no shared mutable state in the language to race
  • ✅ A development is checked file by file in parallel: coq_makefile -j and rocq makefile -j compile independent .v files in separate processes
  • ✅ Asynchronous proofs run in a worker process: -async-proofs on delegates a proof to another process, so a document and the proof that fills it are decoupled
  • ⚠️ The tactic monad threads one proof state: A tactic acts on the current goal, so the tactics in a script are ordered even though the resulting term is pure
  • ⚠️ Parallel checking is a tool option, not a language guarantee: An interactive session with -async-proofs off is sequential, and the option is the user’s choice

1.1.6 Platform

  • ❌ Rocq is not a general-purpose programming language: A term is written to be checked, and Gallina has no I/O, no foreign-function call, and no runtime of its own (P1)
  • ❌ A deployed program exists only in the extraction target: Extraction emits OCaml, Haskell, or Scheme, so one development reaches three ecosystems but the verified artifact runs only as a program in another language (P1)
  • ✅ The checker is an ordinary OCaml program: It builds and runs on the platforms OCaml supports, including Linux, macOS, and Windows
  • ⚠️ The OCaml toolchain is required to build the checker: A plugin or a native_compute build depends on the OCaml environment, not only on Rocq itself

1.1.7 Trade-offs (not coupling)

  • Dependent types trade automation for certainty: The specification lives in the type, and every refinement obligation is discharged by a tactic or by hand
  • The ecosystem is small by scope: Rocq targets verification and mathematics, so a general-purpose library set is out of scope rather than missing
  • The academic audience is the intended one: The domain mark records a scope decision, not a defect of the language
  • Tactic scripts are a workflow choice: Ltac, Ltac2, and ssreflect are ways to construct a term, and a proof can also be written directly as a term
  • Prop erasure is a deliberate design: A proof in Prop is erased from the extracted program, so its cost is a checking cost rather than a runtime cost
  • Totality is required for a consistent logic: The termination obligation is the price of using one language for proofs and for programs

1.2 Ecosystem coupling

1.2.1 Performance

  • ✅ The measured workload is proof checking: The kernel checks a term once, so the checking algorithm, not a program’s runtime, sets the cost
  • ✅ Independent files are checked in parallel: -j and -async-proofs spread a build across the available cores
  • ✅ A heavy reduction can run as compiled code: native_compute evaluates a term at the speed of compiled OCaml
  • ✅ Extracted code runs at the target language’s speed: The deployed program’s performance is the target compiler’s concern
  • ⚠️ Checking time grows with the proof: A large vm_compute, a deep induction, or a long auto search can take minutes, and the cost is paid on every rebuild

1.2.2 Ecosystem

  • ❌ The ecosystem is small and centred on academia: Outside the standard library, mathcomp, and the Rocq Platform, the set of maintained packages is thin (Ec3)
  • ✅ opam installs Rocq, its libraries, and its plugins: The OCaml package manager is the distribution channel
  • ✅ The Rocq Platform pins a compatible set: A Platform release fixes versions of libraries and plugins that are known to work together
  • ✅ The landmark libraries are mature: mathcomp (Mathematical Components), stdpp, and CompCert are long-lived and actively maintained
  • ⚠️ A plugin extends the checker from inside: An OCaml plugin reaches the engine directly, which is powerful and also couples the plugin to a Rocq version

1.2.3 Evolution

  • ✅ The rename from Coq to Rocq preserved compatibility: Rocq 9.0 continued to accept the Coq.* module paths and the coq* command names, so an existing development kept checking
  • ✅ A release is versioned and pinned: opam records the Rocq version and the library versions a development was checked against
  • ✅ Deprecation precedes removal: A renamed tactic or lemma warns before it stops working
  • ✅ The changelog names each change: A release records the renamed lemmas and tactics with their replacements
  • ⚠️ Library and tactic names do move between releases: A development that pins no version may need edits when it is checked under a later Rocq

1.2.4 Domain

  • ❌ The domain is formal verification and mathematics: The language states and checks proofs, and it is not chosen for general software work (D1)
  • ✅ It is a strong fit for the domain it targets: Machine-checked mathematics and verified software are what the system is built to do
  • ✅ The CompCert verified C compiler is a landmark result: A realistic C compiler was proved correct in Coq, which is evidence that the domain fit works at scale
  • ✅ Critical cryptography and kernel components have been verified in it: Rocq has been used to verify cryptographic primitives and operating-system kernel components
  • ✅ Extraction bridges to an industrial artifact: A verified algorithm is extracted to OCaml or Haskell and then deployed
  • ⚠️ A proof of a program is not the program: The extracted code is correct relative to the extracted semantics, and a declared axiom weakens the guarantee

1.2.5 Learning

  • ❌ The learning curve is very steep: Dependent type theory, universes, and the calculus of inductive constructions must be understood before a nontrivial development can be written (L1)
  • ❌ Tactic scripting is a second language: Ltac/Ltac2 and the ssreflect idioms are a distinct skill from writing a term
  • ✅ A first proof is short to write: intros, reflexivity, and Qed complete a small example in the first session
  • ✅ The reference material is thorough and maintained: The Rocq reference manual, the Software Foundations course, and the mathcomp book are stable resources
  • ⚠️ An error message must be read against the goal state: The checker reports a goal and a term, and interpreting the report takes practice

1.2.6 Syntax

  • ✅ The core grammar is small: A term is an application, a fun, a match, or a let, and the proof language is a sequence of commands
  • ✅ Notation and scopes localise a symbol: A notation applies only where its scope is open, so + can mean different things in different developments
  • ✅ Inductive and record declarations read as their structure: Record point := { x : nat; y : nat } names the fields in one line
  • ✅ Proof bullets give a proof a tree shape: -, +, *, and { ... } nest the goals, so the structure is visible
  • ⚠️ Notation interaction is local knowledge: Two declarations for the same infix symbol, with associativity and precedence levels, can parse a term in a way the reader does not expect

1.2.7 Testing

  • ✅ Checking is the test of the proved property: A development that compiles has been checked by the kernel, so the property needs no separate suite
  • ✅ Qed seals a proof and runs the kernel check: The term is re-checked at sealing, independently of the tactics that built it
  • ✅ Fail and Succeed test a command’s outcome: A regression test can require that a specific wrong proof is rejected
  • ✅ Example gives an inline test: An anonymous lemma checks a claim at the point where it is stated
  • ✅ coqdoc renders a checked example into the documentation: A documented example is the same checked term
  • ⚠️ Only the stated property is checked: An Admitted lemma or an Axiom is accepted on trust, so the guarantee holds only over the proved fragment

1.2.8 Security

  • ✅ The kernel check gives the strongest assurance available for the stated property: A Qed term is checked against the calculus, so the result holds as long as the kernel is trusted
  • ✅ Gallina has no memory operation to misuse: There is no pointer arithmetic and no manual free in the logic core
  • ✅ native_compute is opt-in: The compiled reduction is selected explicitly and is disabled by default, so the kernel’s own reduction remains the default path
  • ⚠️ The trusted base includes the kernel, the extraction, and any axiom: A kernel defect, an extraction defect, or a declared axiom is outside the proof
  • ⚠️ Extracted code inherits the target language’s safety: An OCaml or Scheme program is subject to that runtime’s own model

1.3 Engineering readiness

1.3.1 Reproducibility

  • ❌ Builds are not byte-reproducible by default.
  • ❌ Dependencies resolve without a lock by default.

1.3.2 Supply chain

  • ⚠️ Published packages carry no signed provenance by default.
  • ⚠️ The package registry is a flat name space.

1.3.3 Observability

  • ⚠️ No stable tracing and metrics standard.
  • ⚠️ The standard library has no structured logging.

1.3.4 Feedback

  • ✅ No charged mechanism in this dimension.

1.3.5 Interop

  • ❌ No general foreign-function interface.
  • ⚠️ No maintained portable target.

1.3.6 Governance

  • ✅ No charged mechanism in this dimension.

1.4 Profile

Unscored, and kept separate from every score on purpose. The profile records what a mechanism price cannot express: what a running program costs, how well a coding model and an agent work in the language, and whether a safety-critical path exists.

1.4.1 Energy and cost

What this axis asks: what does a running program cost in energy and time?

  • ✅ Compiles to native code: the fastest class in the language energy and time benchmarks [5], [6]. A causal re-analysis attributes the difference to execution time [7].

1.4.2 AI and agent readiness

What this axis asks: how well does a coding model and an agent work in this language?

  • ❌ Sparse training data: models write it unreliably [8].

1.4.3 Safety certification

What this axis asks: is there a certified or standards-qualified path to a safety-critical system?

  • ⚠️ No certified or standards-qualified path for safety-critical systems.

1.5 Scoring detail

1.5.1 Core coupling Dimensions

Dimension Mechanism Description Present Cost
Type T1 dynamic no static check — 0
T2 weak static — 0
T3 dynamic/duck dispatch — 0
T4 no sum types — 0
T5 no generics — 0
T6 no namespaces — 0
T7 type erasure/reflection — 0
T8 operator overloading — 0
T9 inheritance required for polymorphism — 0
T10 no null-safety — 0
T11 no module boundary — 0
T12 no effect tracking — 0
T13 async/sync colouring — 0
T14 unchecked foreign boundary — 0
Type subtotal 0
Construction C1 global mutable state by default — 0
C2 no immutability by default — 0
C3 constructors coupled to allocation — 0
C4 no constructor/validation — 0
Construction subtotal 0
Memory M1 manual deallocation — 0
M2 GC non-deterministic pauses — 0
M3 no RAII — 0
M4 no ownership model — 0
Memory subtotal 0
Error Er1 no structured path — 0
Er2 unchecked exceptions only — 0
Er3 errors ignored/non-exhaustive — 0
Er4 no composable result type — 0
Error subtotal 0
Concurrency K1 GIL/no parallel — 0
K2 shared mutable state default — 0
K3 manual sync no race detection — 0
K4 no structured concurrency — 0
K5 no primitives — 0
Concurrency subtotal 0
Platform P1 cannot function outside one vendor/domain ✅ −15
P2 single-vendor but other uses — 0
P3 legacy/discontinued platform — 0
Platform subtotal −15

Core Dimensions score: 85/100 — total cost = −15 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

1.5.2 Ecosystem coupling Dimensions

Dimension Mechanism Description Present Cost
Performance R1 interpreted no AOT/JIT — 0
R2 GC pauses — 0
R3 JIT warmup — 0
Performance subtotal 0
Ecosystem Ec1 no package manager — 0
Ec2 fragmented tooling — 0
Ec3 small/niche/discontinued ✅ −8
Ec4 proprietary — 0
Ec5 platform-locked tooling — 0
Ec6 monoculture — 0
Ec7 legacy burden — 0
Ecosystem subtotal −8
Evolution V1 breaking changes — 0
V2 frozen — 0
V3 discontinued — 0
V4 glacial standards — 0
Evolution subtotal 0
Domain D1 domain/vendor lock-in ✅ −15
D2 poor domain fit — 0
D3 framework forces architecture — 0
Domain subtotal −15
Learning L1 steep ✅ −8
L2 large surface/multi-paradigm — 0
L3 sparse docs — 0
Learning subtotal −8
Syntax S1 verbose — 0
S2 inconsistent — 0
S3 punctuation-heavy — 0
Syntax subtotal 0
Testing G1 weak tooling — 0
G2 poor debugging — 0
G3 runtime-only errors — 0
Testing subtotal 0
Security Q1 memory-unsafe — 0
Q2 dynamic/weak typing risk — 0
Q3 known vulnerability/injection — 0
Security subtotal 0

Meta Dimensions score: 69/100 — total cost = −31 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

1.5.3 Engineering readiness Dimensions

Dimension Mechanism Description Present Cost
Reproducibility Y1 build not reproducible ✅ −8
Y2 dependencies not pinned ✅ −8
Reproducibility subtotal −15 (−16)
Supply chain Y3 no signed provenance ✅ −8
Y4 registry without namespacing ✅ −4
Supply chain subtotal −12
Observability Y5 no stable tracing standard ✅ −8
Y6 no structured logging ✅ −4
Observability subtotal −12
Feedback Y7 slow build — 0
Y8 no fast in-editor analysis — 0
Feedback subtotal 0
Interop Y9 no foreign-function interface ✅ −8
Y10 no portable target ✅ −4
Interop subtotal −12
Governance Y11 single-vendor governance — 0
Y12 closed specification — 0
Governance subtotal 0

Readiness Dimensions score: 49/100 — total cost = −51 (per-dimension subtotals are capped at −15; an uncapped cost is shown in parentheses where the cap bites).

Verdict: Rocq yields low core coupling for the narrow work it is built for: dependent types put the specification in the type, tactic scripts are separate from the terms they build, extraction decouples verification from the implementation language, and the logic core is pure and total. The core score loses only through P1, because the language does not function outside the domain of formal proof. The platform cost is the price of that focus — a small academic ecosystem, a domain lock-in to verification, and one of the steepest learning curves here. Main strengths: kernel-checked certainty, the CompCert landmark result, and extraction as the bridge to OCaml, Haskell, or Scheme; main weaknesses: the narrow domain, the thin ecosystem, and the depth of type theory and tactic knowledge required.

The formal development. The definitions, theorems, and proofs behind this page are published in:

All published papers

References

[1]
Y. Loth, “On the nature of coupling: All coupling as shared resource access.” Zenodo, Aug. 2026. doi: 10.5281/zenodo.21925122.
[2]
Y. Loth, “Coupling as a consequence of cohesion: Decomposition, the coupling floor, and domain-imposed coupling.” Zenodo, Aug. 2026. doi: 10.5281/zenodo.21925201.
[3]
Y. Loth, “On the nature of cohesion: Cohesion as correctness relative to a partitioning rule.” Zenodo, Jul. 2026. doi: 10.5281/zenodo.21703193.
[4]
The Rocq Development Team, “The rocq reference manual (formerly Coq).” Rocq, 2024. Available: https://coq.inria.fr/
[5]
R. Pereira et al., “Energy efficiency across programming languages: How do energy, time, and memory relate?” in Proceedings of the 10th ACM SIGPLAN international conference on software language engineering (SLE), 2017, pp. 256–267. doi: 10.1145/3136014.3136031.
[6]
R. Pereira et al., “Ranking programming languages by energy efficiency,” Science of Computer Programming, 2021, doi: 10.1016/j.scico.2021.102609.
[7]
N. van Kempen, H.-J. Kwon, D. T. Nguyen, and E. D. Berger, “It’s not easy being green: On the energy efficiency of programming languages,” in Proceedings of the 40th IEEE/ACM international conference on automated software engineering (ASE), 2025. doi: 10.1109/ASE63991.2025.00131.
[8]
S. Joel, J. J. Wu, and F. H. Fard, “A survey on LLM-based code generation for low-resource and domain-specific programming languages,” ACM Transactions on Software Engineering and Methodology, 2025, doi: 10.1145/3770084.