形式仕様記述はなぜ有用か

http://iiyu.asablo.jp/blog/2006/08/20/491884
ここを読むとなんとなく、腑に落ちるような気もします。

ひとまず、抜粋。

それまで自然言語やUMLで仕様記述をやってきてバグがつぶせない
ので、形式仕様記述言語VDM++で形式仕様記述を実践して大きな成果を挙げた
のです。すごいのが、VDM++で10万行も書いてること。＼(^O^)／
　これで、実装前、すなわち仕様の段階で350件ほどのバグを潰してます。

VDM++やBメソッドを今後学習するので、
学習した上で、自分なりの意見を整理したいところ。