bloomberg

crane

C++2026–2026

bloomberg / crane

crane

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

Explore on GitHub Read Hacker News discussions

4Distinct people

4Mentions

0Explicit recommenders

174GitHub stars

REPOSITORY AT A GLANCE

What to know before exploring

What it is

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

GitHub

Where it is used

No documented product use has been verified yet.

What people are saying

No recommendation phrase was found in the indexed comments.

No classified warning is attached to this page. Read the discussions before treating silence as approval.

Also in these discussions

No other repository is repeatedly linked in the same discussions.

This week on Hacker News

Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 3:56:07 PM UTC.

No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.

Mentions over time

HN mentions by 3-hour interval4 dated mentions

Observed mentions: 2026-01-24 07:47:01 UTC to 2026-01-26 18:34:18 UTC.

Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.

View mention counts and date ranges

UTC ranges include their start and exclude their end. Select a period to filter the source evidence.
Period	Start (UTC)	End (exclusive, UTC)	Mentions	Comments
Jan 24, 06:00	2026-01-24 06:00:00 UTC	2026-01-24 09:00:00 UTC	1	1
Jan 24, 09:00	2026-01-24 09:00:00 UTC	2026-01-24 12:00:00 UTC	1	1
Jan 24, 12:00	2026-01-24 12:00:00 UTC	2026-01-24 15:00:00 UTC	0	0
Jan 24, 15:00	2026-01-24 15:00:00 UTC	2026-01-24 18:00:00 UTC	1	1
Jan 24, 18:00	2026-01-24 18:00:00 UTC	2026-01-24 21:00:00 UTC	0	0
Jan 24, 21:00	2026-01-24 21:00:00 UTC	2026-01-25 00:00:00 UTC	0	0
Jan 25, 00:00	2026-01-25 00:00:00 UTC	2026-01-25 03:00:00 UTC	0	0
Jan 25, 03:00	2026-01-25 03:00:00 UTC	2026-01-25 06:00:00 UTC	0	0
Jan 25, 06:00	2026-01-25 06:00:00 UTC	2026-01-25 09:00:00 UTC	0	0
Jan 25, 09:00	2026-01-25 09:00:00 UTC	2026-01-25 12:00:00 UTC	0	0
Jan 25, 12:00	2026-01-25 12:00:00 UTC	2026-01-25 15:00:00 UTC	0	0
Jan 25, 15:00	2026-01-25 15:00:00 UTC	2026-01-25 18:00:00 UTC	0	0
Jan 25, 18:00	2026-01-25 18:00:00 UTC	2026-01-25 21:00:00 UTC	0	0
Jan 25, 21:00	2026-01-25 21:00:00 UTC	2026-01-26 00:00:00 UTC	0	0
Jan 26, 00:00	2026-01-26 00:00:00 UTC	2026-01-26 03:00:00 UTC	0	0
Jan 26, 03:00	2026-01-26 03:00:00 UTC	2026-01-26 06:00:00 UTC	0	0
Jan 26, 06:00	2026-01-26 06:00:00 UTC	2026-01-26 09:00:00 UTC	0	0
Jan 26, 09:00	2026-01-26 09:00:00 UTC	2026-01-26 12:00:00 UTC	0	0
Jan 26, 12:00	2026-01-26 12:00:00 UTC	2026-01-26 15:00:00 UTC	0	0
Jan 26, 15:00	2026-01-26 15:00:00 UTC	2026-01-26 18:00:00 UTC	0	0
Jan 26, 18:00	2026-01-26 18:00:00 UTC	2026-01-26 21:00:00 UTC	1	1

What Hacker News says

4 sources

GregarianChild·Jan 26, 2026

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 easier for handling non-determinism?

In Extracting verified C++ from the Rocq theorem prover at Bloomberg

aleksejs·Jan 24, 2026

The linked website and repository do not refer to the outputs as "verified C++". The use of that term in the submission title here seems misleading, and the Design Principles [1] document clarifies it is only the source (Rocq) programs that are formally verified. It seems far from obvious that the complex and ad-hoc syntactic transformations involved in translating them to C++ preserve the validity of the source proofs. [1] https://github.com/bloomberg/crane/wiki/Design-Principles

In Extracting verified C++ from the Rocq theorem prover at Bloomberg

joomy·Jan 24, 2026

Hi, I'm one of Crane's developers. You can map Rocq `bool`s to C++ `bool`, 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 of the tests that do not yet pass. But then again, in the readme, we are upfront with these issues: > Crane is under active development. While many features are functional, parts of the extraction pipeline are still experimental, and you may encounter incomplete features or unexpected behavior. Please report issues on the GitHub tracker. I should also note, mapping Rocq types to ideal C++ types is only one part of it. There are still efficiency concerns with recursive functions, smart pointers, etc. This is an active research proj

Read the rest

ect, and we have plans to tackle these problems: for recursion: try CPS + defunctionalization + convert to loops, for smart pointers: trying what Lean does (https://dl.acm.org/doi/10.1145/3412932.3412935), etc.

In Extracting verified C++ from the Rocq theorem prover at Bloomberg

seeknotfind·Jan 24, 2026

From tests/basics/levenshtein/levenshtein.cpp: struct Ascii { std::shared_ptr<Bool0::bool0> _a0; std::shared_ptr<Bool0::bool0> _a1; std::shared_ptr<Bool0::bool0> _a2; std::shared_ptr<Bool0::bool0> _a3; std::shared_ptr<Bool0::bool0> _a4; std::shared_ptr<Bool0::bool0> _a5; std::shared_ptr<Bool0::bool0> _a6; std::shared_ptr<Bool0::bool0> _a7; }; This is ... okay, if you like formal systems, but I wouldn't call it performant. Depending on what you are doing, this might be performant. It might be performant compared to other formally verified alternatives. It's certainly a lot nicer than trying to verify something already written in C++, which is just messy. From theories/Mapping/NatIntStd.v: - Since [int] is bounded while [nat] is (theoretically) infinite, you have to make sure

Read the rest

by yourself that your program will not manipulate numbers greater than [max_int]. Otherwise you should consider the translation of [nat] into [big_int]. One of the things formal verification people complain about is that ARM doesn't have a standard memory model, or CPU cache coherence is hard to model. I don't think that's what this 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 in the style of CompCert. What this means is that you can formalize things, and you can have assurances, but then sometimes things may still break in weird ways if you do weird things? Well, that happens no matter what you do. This is a noble effort bridging two worlds. It's cool. It's refreshing to see a "simpler" approach. Get some of the benefits of formal verification without all the hassle.

In Extracting verified C++ from the Rocq theorem prover at Bloomberg