clarus Karma 269 Created 14 years ago Recent Submissions 1. ▲ Extracting verified C++ from the Rocq theorem prover at Bloomberg (bloomberg.github.io) 129 points · 1 month ago · 39 comments All submissions on HN · View profile on HN