Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

bloomberg.github.io

Post reply on HN
Print view View original

21–30 of 41 posts

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

#21

Post by riedel »

aleksejs wrote: post #18

The linked website and repository do not refer to the outputs as "verified C++". The use of that term in the submission title here seems misleading, and the Design Principles [1] document clarifies it is only the source (Rocq) programs that are formally verified. It seems far from obvious that the complex and ad-hoc syntactic transformations involved in translating them to C++ preserve the validity of the source proo…

Well the title of the paper is >Crane Lowers Rocq Safely into C++

So 'safely' implies somehow that they care about not destroying guarantees during their transformation. To me as a layperson (I studied compiler design and formal verification some.long time ago, but have little to zero experience) it seems at easier to write a set of correct transformations then to formalize arbitrary C++ code.

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

#22

Post by aleksejs »

riedel wrote: post #21
aleksejs wrote: post #18

The linked website and repository do not refer to the outputs as "verified C++". The use of that term in the submission title here seems misleading, and the Design Principles [1] document clarifies it is only the source (Rocq) programs that are formally verified. It seems far from obvious that the complex and ad-hoc syntactic transformations involved in translating them to C++ preserve the validity of the source proo…

Well the title of the paper is >Crane Lowers Rocq Safely into C++ So 'safely' implies somehow that they care about not destroying guarantees during their transformation. To me as a layperson (I studied compiler design and formal verification some.long time ago, but have little to zero experience) it seems at easier to write a set of correct transformations then to formalize arbitrary C++ code.

How do you even begin to define what correctness means for the transformations if you have no formalized model of the thing you're transforming into?

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

#23

Post by bluGill »

zozbot234 wrote: post #20
bluGill wrote: post #19

Earlier quoted context omitted.

60% of the effort is testing to ensure it works correctly.

AI agents test their code too, that's how they ensure that they've got the right solution at the end of the day. With an existing implementation in C++ the task would be incredibly easy for them.

You have far too much trust in automated tests.

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

#24

Post by joomy »

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.

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

#25

Post by joomy »

aleksejs wrote: post #18

The linked website and repository do not refer to the outputs as "verified C++". The use of that term in the submission title here seems misleading, and the Design Principles [1] document clarifies it is only the source (Rocq) programs that are formally verified. It seems far from obvious that the complex and ad-hoc syntactic transformations involved in translating them to C++ preserve the validity of the source proo…

Yes, we were careful not to call it that. I still don't mind calling our programs verified, since they are verified in Rocq and we do our best to preserve the semantics of them. Right now the only measure we have is testing a small set of programs and also carefully picking a subset of C++ that we trust. Our future plan is to generate random Rocq programs, extract them via Crane, and compare the output to the outputs of extraction to OCaml, and even CertiCoq, which is a verified compiler from Rocq to C, (mostly) proven correct with respect to CompCert semantics.

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

#26

Post by joomy »

aleksejs wrote: post #22
riedel wrote: post #21

Earlier quoted context omitted.

Well the title of the paper is >Crane Lowers Rocq Safely into C++ So 'safely' implies somehow that they care about not destroying guarantees during their transformation. To me as a layperson (I studied compiler design and formal verification some.long time ago, but have little to zero experience) it seems at easier to write a set of correct transformations then to formalize arbitrary C++ code.

How do you even begin to define what correctness means for the transformations if you have no formalized model of the thing you're transforming into?

This is another reason we are being careful with the correctness claim. The closest project I know right now that comes close to a formalized model of C++ is the BRiCk project:

https://skylabsai.github.io/BRiCk/index.html

https://github.com/SkyLabsAI/BRiCk

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

#27

Post by joomy »

seeknotfind wrote: post #15
joomy wrote: post #5

Earlier quoted context omitted.

Hi, I'm one of Crane's developers. You can map Rocq `bool`s to C++ `bool`, Rocq strings to C++ `std::string`s, etc. You just have to manually import the mapping module: https://github.com/bloomberg/crane/blob/6a256694460c0f895c27... The output you posted is from an example that we missed importing. It's also one of the tests that do not yet pass. But then again, in the readme, we are upfront with these issues: > Cran…

Thanks, yeah, I did see some of the pure C++ types getting converted. Though it makes a lot of sense why you had to go with shared_ptr for generic inductive types. Have you considered combinatorial testing? Test code generation for each sample program, for each set of mappings, and ensure they all have the same behavior. If you look at the relative size or performance, it could allow you to automatically discover thi…

> Have you considered combinatorial testing?

Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and even CertiCoq. But fixing a program and trying different mappings would certainly be a useful tool for any dev who would like to use our tool, and we should put it on our roadmap.

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

#28

Post by seeknotfind »

joomy wrote: post #27
seeknotfind wrote: post #15

Earlier quoted context omitted.

Thanks, yeah, I did see some of the pure C++ types getting converted. Though it makes a lot of sense why you had to go with shared_ptr for generic inductive types. Have you considered combinatorial testing? Test code generation for each sample program, for each set of mappings, and ensure they all have the same behavior. If you look at the relative size or performance, it could allow you to automatically discover thi…

> Have you considered combinatorial testing? Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and even CertiCoq. But fixing a program and trying different mappings would certainly be a useful tool for any dev who would like to use our tool, and we should put it on our roadmap.

Very cool. Can't wait to see what's next with this project! Congrats on the huge scale of tests/examples as well.

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

#29

Post by csto12 »

joomy wrote: post #27
seeknotfind wrote: post #15

Earlier quoted context omitted.

Thanks, yeah, I did see some of the pure C++ types getting converted. Though it makes a lot of sense why you had to go with shared_ptr for generic inductive types. Have you considered combinatorial testing? Test code generation for each sample program, for each set of mappings, and ensure they all have the same behavior. If you look at the relative size or performance, it could allow you to automatically discover thi…

> Have you considered combinatorial testing? Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and even CertiCoq. But fixing a program and trying different mappings would certainly be a useful tool for any dev who would like to use our tool, and we should put it on our roadmap.

Are LLMs part of your development workflow for something like this? If they are, is it through something like Claude Code or something else?

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

#30

Post by GregarianChild »

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.

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 |= phi and extr(P, phi) = (P', phi') then not just

    semantics(P) == semantics(P')
as in compilation, but also

    semantics(phi) = semantics(phi'),
hence P' |= phi'.

I say "at least conceptually" above, because this specificatyion is often not lowered into a different logical formalism. Instead it is implied / assumed that if the extraction mechanism was correct, then the specification could also be lowered ...

Post reply on HN