Crane Lowers Rocq Safely into C++
summary
Crane extracts Rocq into idiomatic, readable C++ that maps Rocq inductive types and monadic effects to either stdlib or Bloomberg core types, generates pattern-match via std::variant + visit, and uses iTrees for monadic effects. A software transactional memory runtime is implemented and a concurrent hash table is extracted to C++ and compiles, though the implementation is not yet formally verified; correctness is checked via differential testing and standard CI. The tool supports custom extraction mappings and targets software transactional memory semantics, with planned CPS/defunctionalization for speed.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:30Crane tool overview
- 3:17Extracting C++ from Rocq
- 7:31Customizing extraction
- 10:03Monadic effects handling
- 12:31Verified concurrent programming
- 14:42Safety guarantees
- 16:28Q&A
related talks
15mECROs: Building Global Scale Systems from Sequential Code
31mSafe Software for Autonomous Mobility With Modern C++
39mTemporal Dynamics - Exploring the Intricacies of Object Lifetimes in Modern C++
01h 21mAfter Reflection: The Runtime Story
54mC++ Common Knowledge
58m“Embracing Standard C++ for the Windows Runtime"
01h 13mPractical Production-Proven Constexpr API Elements
18mRecursion schemes in OCaml: An experience report