そりゃごっちゃにすべきじゃない文脈もあるだろうが

C言語の喩えで言えば
gccもVCも対応していない機能はないようなものでしょ

C言語の仕様策定は実装ありきだから
そのうち対応する見込みはあるけど
VDMで証明とかOverture界隈も興味の対象から外れている感じだし先が見えん