alt Hacker NewsA 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.
Would be interesting to see how performant it is (or how easily you can write performant code).