WingNews logo WingNews
top | item 46689631

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

129 points| clarus | 1 month ago |bloomberg.github.io

39 comments

order

zero-sharp|1 month ago

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 finite set of inputs. It cannot rule out bugs across all possible executions. To obtain stronger guarantees, we turn to formal verification, and in particular to certified programming techniques that allow us to de- velop programs alongside mathematical proofs of their correctness. However, there is a significant gap between the languages used to write certified programs and those relied upon in production systems. Bridging this gap is crucial for bringing the benefits of formal verification into real-world software systems.

cobbal|1 month ago

That's essentially correct. Extraction is a term in roqc. A rocq program contains both a computational part, and proofs about that computation, all mixed together in the type system. Extraction is the automated process of discarding the proofs and writing out the computational component to a more conventional (and probably more efficient) programming language.

The original extractor was to ocaml, and this is a new extractor to c++.

joomy|1 month ago

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.

clarus|1 month ago

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

Interestingly, this can be integrated into production system to quickly formally verify critical components while being fully compatible with the existing Bloomberg's C++ codebase.

InkCanon|1 month ago

Would be interesting to see how performant it is (or how easily you can write performant code).

aleksejs|1 month ago

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 proofs.

[1] https://github.com/bloomberg/crane/wiki/Design-Principles

riedel|1 month ago

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.

joomy|1 month ago

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.

zozbot234|1 month ago

Why does it have to be C++? Can the extraction strategy be ported to Rust? Rust is just getting a lot more attention from formal methods folks in general, and has good basic interop with C.

bluGill|1 month ago

I have 10s of millions of lines of C++. It cost nearly a billion dollars to write it, starting before Rust existed. Rewriting in rust would cost more (inflation more than eats up any productivity gains - if we were to rewrite we would fix architectural mistakes we now know we made so a of this wouldn't be a straight rewrite slightly increasing costs, but safe rust wouldn't even be possible with some things anyway)

erichocean|1 month ago

Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.

benreesman|1 month ago

I mostly write lean4 now and emit proof-carrying System F Omega via rfl. It's the right level of abstraction when the droids have been pinned to theory laden symbolisms. It's also just pleasant to use.