With what, Frama-C? Good luck getting it adopted outside domains that enforce its use for code certification.
You are right that after having proven your code correct, you might want to use an implementation (compiler or interpreter), that is also proven correct. But those are still two different things.
But I agree that C is not the best language for writing critical code.