> rather than having to translate the whole program into Rocq

Translating your program to Rocq is vastly easier than to write a proof for a binary.