3 ms·
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 tran
by riedel 9mo 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.
- aleksejs 9mo agoHow 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?
- joomy 9mo agoThis 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://skylabsai.github.io/BRiCk/index.html https://github.com/SkyLabsAI/BRiCk https://github.com/SkyLabsAI/BRiCk