bloomberg/crane
View on GitHub ↗ ★ 174 C++
A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.
4 mentions on Hacker News by 4 people: 0 stories, 4 comments · first 2026-01-24 · latest 2026-01-26
20082026
-
Thanks. I hope you publish this. I imagine https://github.com/bloomberg/crane/blob/main/theories/Monads... is the functional specification of STM. I see that you use ITrees. WHat's the reason for not using Choice Trees that tend to be…
comment by GregarianChild · 2026-01-26 · in Extracting verified C++ from the Rocq theorem prover at Bloomberg -
…transformations involved in translating them to C++ preserve the validity of the source proofs. [1] https://github.com/bloomberg/crane/wiki/Design-Principles
comment by aleksejs · 2026-01-24 · in Extracting verified C++ from the Rocq theorem prover at Bloomberg -
…Rocq strings to C++ `std::string`s, etc. You just have to manually import the mapping module: https://github.com/bloomberg/crane/blob/6a256694460c0f895c27... The output you posted is from an example that we missed importing. It's also one…
comment by joomy · 2026-01-24 · in Extracting verified C++ from the Rocq theorem prover at Bloomberg -
…project is about. This project is having basically provable code. They also say this in their wiki: https://github.com/bloomberg/crane/wiki/Design-Principles#4-... > Crane deliberately does not start from a fully verified compiler pipeline…
comment by seeknotfind · 2026-01-24 · in Extracting verified C++ from the Rocq theorem prover at Bloomberg