So Rust has unsafe code blocks that you use when you can't use the type system to enforce that a piece of code is safe. I wonder if would be viable to write tho

So Rust has unsafe code blocks that you use when you can't use the type system to enforce that a piece of code is safe. I wonder if would be viable to write those things in ATS with all the proofs to guarantee that the code is safe, compile to C and then call that trusted C code through the FFI? It might not work in all cases, since I have the impression that unsafe Rust code is even more expressive when it comes to low level code (I guess this also means more unsafe) than C.