Discussion: doc-verification-bridge

Stream: general

[Bas Spitters]

This looks exciting.

Your main example of a bridge, is an example of reflection in type theory, as it is used in the Rocq SSReflect language and the (huge) mathematical components library. Did you intend to capture the same concept ?

[Notification Bot]

This topic was moved here from #announce > doc-verification-bridge by Floris van Doorn.

[Nicolas Rouquette]

Thanks for the connection to SSReflect! I'm unfamiliar with the Rocq SSReflect language—could you point me to key references on how reflection is organized there? I'd be curious whether there's an existing taxonomy of theorem types that relates to what I'm trying to capture.

To clarify the distinction I'm drawing: the "bridging" concept is specifically about connecting two fundamentally different kinds of formalization:

• Mathematical (Prop-based): focused on proving properties—specifications that may not be computable
• Computational (Bool-based): focused on implementing functions that have proven properties

This is distinct from refinement within the mathematical world (e.g., abstract algebra → concrete representation, or high-level spec → low-level spec). Both sides remain in Prop for that kind of refinement.

The Prop/Bool bridge is special because it crosses the specification/implementation divide—it is about connecting "what should hold" (a proposition) with "how to check it" (executable code). The tool's validates relationship specifically tracks which Bool functions have been proven correct against which Prop specifications.

My motivation came from my own experience: after developing mathematical formalizations to support refinement-style proofs of a computational implementation, I found it difficult to track which properties of the implementation were actually verified and how the mathematical formalization supported that verification. I needed a way to assess progress and strategize what to focus on next—informed by which properties of the implementation are important to verify and which remain unverified.

In the paper, I follow @Markus Himmel's framing from "Proofs for Programs, Programs for Proofs":

• Validation bridges: f x = true → P x (computed results can be trusted)
• Specification bridges: P x → f x = true (proofs can leverage native_decide)

I'd love to learn more about how SSReflect/Mathematical Components organizes these patterns—are there papers or documentation that discuss their reflection methodology systematically?

[Bas Spitters]

There's a book :-) https://math-comp.github.io/mcb/

There is a long history, but at least:
Gonthier, G. (2005). A computer-checked proof of the Four Colour Theorem.
Gonthier, G., Mahboubi, A., & Tassi, E. (2008). A Small Scale Reflection extension for the Coq system.