We are at 33%, still far from completion, but many instructions are similar!
The "coq-of-rust" translator gives us a first representation of the code in Rocq, but then we need to show that a typing of the translated code exists, which can require a bit of work.
The "coq-of-rust" translator gives us a first representation of the code in Rocq, but then we need to show that a typing of the translated code exists, which can require a bit of work.
Comments
We are not yet there, but hopefully, it will be the case in some months!