Comment by riedel
1 month ago
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.
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?
This is another reason we are being careful with the correctness claim. The closest project I know right now that comes close to a formalized model of C++ is the BRiCk project:
https://skylabsai.github.io/BRiCk/index.html
https://github.com/SkyLabsAI/BRiCk