Comment Comment by m1el > rather than having to translate the whole program into RocqTranslating your program to Rocq is vastly easier than to write a proof for a binary. parent m1el 11 days ago
Translating your program to Rocq is vastly easier than to write a proof for a binary.