Comment by zozbot234
3 hours 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.
3 hours 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.
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.
60% of the effort is testing to ensure it works correctly.
1 reply →