VDMの存在意義が良くわからない

仕様記述言語 VDM というものを勉強させていただいています。仕様記述なので「プログラム的に書いた仕様書」であり、この時点で論理的なエラーがないか検出するためのもの見たいなのですが…

結局これ「言語」なんで、ガリゴリコード書いていく形っぽいんですよ。

となると、今まで普通にコード書いてきたのと何が違うのかさっぱりわからない。 人間の手でコードを打っていく以上、絶対にいつか誤爆る == 仕様ミスが出てくる ような気がするんですが…。＾＾；

人が書くソースコードには問題が入りやすい故に、ソースコード自動生成化ツールとか発展しつつあるのに「ソースを書く為にソースを書かせる」ってのは何なんだろうか…。素でよくわからないのかしら…。