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

▲

riedel 2 hours ago | parent [-]

Well the title of the paper is >Crane Lowers Rocq Safely into C++

So 'safely' implies somehow that they care about not destroying guarantees during their transformation. To me as a layperson (I studied compiler design and formal verification some.long time ago, but have little to zero experience) it seems at easier to write a set of correct transformations then to formalize arbitrary C++ code.

	▲	aleksejs 2 hours ago \| parent [-]
		How do you even begin to define what correctness means for the transformations if you have no formalized model of the thing you're transforming into?