Extracting verified C++ from the Rocq theorem prover at Bloomberg
2 months ago
- #C++ extraction
- #Crane
- #Rocq
- Latest version of Crane is alpha
- Explore common topics, guides, and documentation for Crane
- Install Crane, configure Rocq, and run your first extraction
- Understand the goals and tradeoffs behind Crane's C++ extraction strategy
- Browse example Rocq projects and extracted C++ code
- Learn about all Crane options, extraction rules, and flags
- Discover the Rocq library of types, monads, etc. used from extracted code
- Check out planned features and upcoming improvements