I fully expect formally verified C to become the standard for any reasonably critical software. It's astonishing how easy it is to crank out program equivalence proofs these days...