| ▲ | zozbot234 5 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. | |||||||||||||||||||||||||||||||||||
| ▲ | joomy 5 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 4 hours ago | parent | prev | next [-] | ||||||||||||||||||||||||||||||||||
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) | |||||||||||||||||||||||||||||||||||
| |||||||||||||||||||||||||||||||||||
| ▲ | 5 hours ago | parent | prev [-] | ||||||||||||||||||||||||||||||||||
| [deleted] | |||||||||||||||||||||||||||||||||||