| ▲ | Extracting verified C++ from the Rocq theorem prover at Bloomberg(bloomberg.github.io) |
| 103 points by clarus 4 days ago | 19 comments |
| |
|
| ▲ | zero-sharp an hour ago | parent | next [-] |
| 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 an hour ago | parent [-] | | 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++. |
|
|
| ▲ | aleksejs an hour ago | parent | prev | next [-] |
| 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 16 minutes ago | parent [-] | | 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. |
|
|
| ▲ | clarus 4 days ago | parent | prev | next [-] |
| 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 11 hours ago | parent [-] | | Would be interesting to see how performant it is (or how easily you can write performant code). | | |
| ▲ | seeknotfind 11 hours ago | parent [-] | | From tests/basics/levenshtein/levenshtein.cpp: struct Ascii {
std::shared_ptr<Bool0::bool0> _a0;
std::shared_ptr<Bool0::bool0> _a1;
std::shared_ptr<Bool0::bool0> _a2;
std::shared_ptr<Bool0::bool0> _a3;
std::shared_ptr<Bool0::bool0> _a4;
std::shared_ptr<Bool0::bool0> _a5;
std::shared_ptr<Bool0::bool0> _a6;
std::shared_ptr<Bool0::bool0> _a7;
};
This is ... okay, if you like formal systems, but I wouldn't call it performant. Depending on what you are doing, this might be performant. It might be performant compared to other formally verified alternatives. It's certainly a lot nicer than trying to verify something already written in C++, which is just messy.From theories/Mapping/NatIntStd.v: - Since [int] is bounded while [nat] is (theoretically) infinite,
you have to make sure by yourself that your program will not
manipulate numbers greater than [max_int]. Otherwise you should
consider the translation of [nat] into [big_int].
One of the things formal verification people complain about is that ARM doesn't have a standard memory model, or CPU cache coherence is hard to model. I don't think that's what this project is about. This project is having basically provable code. They also say this in their wiki:https://github.com/bloomberg/crane/wiki/Design-Principles#4-... > Crane deliberately does not start from a fully verified compiler pipeline in the style of CompCert. What this means is that you can formalize things, and you can have assurances, but then sometimes things may still break in weird ways if you do weird things? Well, that happens no matter what you do. This is a noble effort bridging two worlds. It's cool. It's refreshing to see a "simpler" approach. Get some of the benefits of formal verification without all the hassle. | | |
| ▲ | joomy 7 hours ago | parent [-] | | 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: > Crane is under active development. While many features are functional, parts of the extraction pipeline are still experimental, and you may encounter incomplete features or unexpected behavior. Please report issues on the GitHub tracker. I should also note, mapping Rocq types to ideal C++ types is only one part of it. There are still efficiency concerns with recursive functions, smart pointers, etc. This is an active research project, and we have plans to tackle these problems: for recursion: try CPS + defunctionalization + convert to loops, for smart pointers: trying what Lean does (https://dl.acm.org/doi/10.1145/3412932.3412935), etc. | | |
| ▲ | seeknotfind an hour ago | parent [-] | | 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 this issue. Also, allocation counting. Hey also sucks you are not in SF. I'm looking for people into formalization in the area, but I haven't found any yet |
|
|
|
|
|
| ▲ | zozbot234 3 hours ago | parent | prev | next [-] |
| 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. |
| |
| ▲ | joomy 3 hours ago | parent | next [-] | | We do C++ only because C++ is the primary programming language at Bloomberg, and we aim to generate verified libraries that interact easily with the existing code. More about our design choices can be found here: https://bloomberg.github.io/crane/papers/crane-rocqpl26.pdf | |
| ▲ | bluGill 2 hours ago | parent | prev [-] | | 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) | | |
| ▲ | zozbot234 an hour ago | parent [-] | | Cutting edge AI agents would eat 10 MLOC for breakfast. That's a trivial workload, especially for a rewrite that's not intended to involve any new semantics. | | |
| ▲ | bluGill an hour ago | parent [-] | | 60% of the effort is testing to ensure it works correctly. | | |
| ▲ | zozbot234 an hour ago | parent [-] | | 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. |
|
|
|
|
|
| ▲ | throw567643u8 4 hours ago | parent | prev | next [-] |
| Where is this team based? Was curious if it was the London office. |
| |
|
| ▲ | erichocean 3 hours ago | parent | prev [-] |
| Getting the AI to work with Rocq is a useful goal, Lean has been useful so far. |
| |
| ▲ | benreesman an hour ago | parent [-] | | 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. |
|
