Extracting verified C++ from the Rocq theorem prover at Bloomberg

Post by GregarianChild » Sun, Jan 25, 2026, 5:37 PM UTC

joomy wrote: post #24

zero-sharp wrote: post #14

If I understand this correctly, it translates Rocq to C++? Took me several minutes to even understand what this is. Why is it called an extraction system? Who is this for? I'm confused. edit: I had to dig into the author's publication list: https://joomy.korkutblech.com/papers/crane-rocqpl26.pdf Testing remains a fundamental practice for building confidence in software, but it can only establish correctness over a fi…

Just like JavaScript folks like calling their compilers "transpiler", proof assistants folks like calling their compilers "extraction". Essentially it's a compiler from a high-level language to a slightly lower-level, but still reasonably high-level language.

Post by joomy » Sun, Jan 25, 2026, 11:37 PM UTC

GregarianChild wrote: post #31

joomy wrote: post #24

Earlier quoted context omitted.

Just like JavaScript folks like calling their compilers "transpiler", proof assistants folks like calling their compilers "extraction". Essentially it's a compiler from a high-level language to a slightly lower-level, but still reasonably high-level language.

I have another question, the abstract of your paper says that you "provide concurrency primitives in Rocq" . But this is not really explained in the text. What are those "concurrency primitives"?

Post by GregarianChild » Mon, Jan 26, 2026, 12:49 PM UTC

joomy wrote: post #32

GregarianChild wrote: post #30

Earlier quoted context omitted.

I would phrase it a little different. Simplifying a bit, a compiler tr(.) translates from a source language L1 to a target language L2 such that semantics(P) == semantics(tr(P)) for all programs in L1. In contrast, and again simplifying a bit, extraction extr(.) assumes not only language L1 and L2 as above, but, at least conceptually, also corresponding specification languages S1 and S2 (aka logics). Whenever P |= ph…

I'm not entirely sure I fully agree with this definition; it seems somewhat arbitrary to me. Where is this definition from? My usual intuition is whether the generated code at the end needs a complicated runtime to replicate the source language's semantics. In Crane, we avoid that requirement with smart pointers, for example.

Post by GregarianChild » Mon, Jan 26, 2026, 6:34 PM UTC

mzweav wrote: post #36

GregarianChild wrote: post #34

Earlier quoted context omitted.

Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.

I'm the other dev of Crane. Our current plan is to use BRiCk ( https://skylabsai.github.io/BRiCk/index.html ) to directly verify that the C++ implementation our STM primitives are extracted to matches the functional specification of STM. Having done that, we can then axiomatize the functional specification over our monadic, interaction tree interface and reason directly over the functional code in Rocq without needin…

Post by GregarianChild » Tue, Jan 27, 2026, 1:33 PM UTC

joomy wrote: post #38

GregarianChild wrote: post #37

Earlier quoted context omitted.

Thanks. I hope you publish this. I imagine https://github.com/bloomberg/crane/blob/main/theories/Monads... is the functional specification of STM. I see that you use ITrees. WHat's the reason for not using Choice Trees that tend to be easier for handling non-determinism?

Our 2 page extended abstract was more like a preannouncement. We hope to have a draft of the full paper by the end of the year. And we're not opposed to choice trees. I personally am not too familiar with them but there's time to catch up on literature. :)

    CoInductive itree (E : Type -> Type) (R : Type) : Type :=
    | Ret (r : R)                                                                                                                                                                                                         
    | Tau (t : itree E R)                                                                                                                                                                                                 
    | Vis {T : Type} (e : E T) (k : T -> itree E R)                                                                                                                                                                       

    CoInductive ctree (E : Type -> Type) (C : Type -> Type) (R : Type) : Type :=
    | Ret (r : R)                                                                                                                                                                                                         
    | Tau (t : ctree E C R)                                                                                                                                                                                               
    | Vis {T : Type} (e : E T) (k : T -> ctree E C R)                                                                                                                                                                     
    | Choice {T : Type} (c : C T) (k : T -> ctree E C R)