>>187,188
現実世界を抽象化する過程に意味が伴うのはその通りで、視覚化手法も形式手法も同じ
形式手法にとっても抽象化の過程ではコトバの意味が大切なのに変わりはない

違うのは、抽象化の成果物である「仕様(設計書)の検証」において、視覚化手法では
(人間が介在する)直感を頼りとしており、そこではコトバの意味が重要な位置を占める
それに対して形式手法では仕様の検証に人の直感は介在せず、コトバの意味は無視する
ここで、証明(=形式を元にした検証)を人力でやろうが証明器で自動化しようが同じ

そして、もし証明が失敗すれば(仕様に矛盾を発見すれば)、現実世界の抽象化という前工程に立ち返る
その時には、(数学としての)形式化の単純ミスもあるだろうけど、コトバの意味(の定義)の過ち、
つまり(抽象化の過程で)現実世界の解釈に何か誤りや漏れがあったことが発見できるだろう