Does that mean I can use C + Frama-C so I won't have to use Rust (or Ada / SPARK)? :P