I meant integrating it into FFI's expecting C code. It's true that it makes stronger guarantees. I have a concept also that's called Brute Force Assurance where

I meant integrating it into FFI's expecting C code. It's true that it makes stronger guarantees. I have a concept also that's called Brute Force Assurance where one source gets converted into Rust, Frama-C, and SPARK. Idea is static analysis tools for each knock out errors others can't catch. Final result is portable C.