What is the benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)
Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.