Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.
Extracting verified C++ from the Rocq theorem prover at Bloomberg
11–20 of 41 posts
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#12Why 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.
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)
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#13Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.
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.
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#14If 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.
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#15Earlier quoted context omitted.
From tests/basics/levenshtein/levenshtein.cpp: struct Ascii { std::shared_ptr _a0; std::shared_ptr _a1; std::shared_ptr _a2; std::shared_ptr _a3; std::shared_ptr _a4; std::shared_ptr _a5; std::shared_ptr _a6; std::shared_ptr _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 formal…
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 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
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#16Why 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.
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)
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.
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#17If 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…
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++.
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#18The 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
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#19Earlier quoted context omitted.
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)
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.
60% of the effort is testing to ensure it works correctly.
Re: Extracting verified C++ from the Rocq theorem prover at Bloomberg
#20Earlier quoted context omitted.
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.
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.