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