エラーや例外が発生しないプログラムが必ずしも「正しい」訳じゃないように
形式的に無矛盾な仕様が必ずしも「正しい」訳じゃない

無矛盾な証券決済システムの仕様は
鉄道運行管理システムの仕様としては全くもって正しくない

記号を記号として扱うのは機械でもできるし機械の方が得意だ
しかし形式意味論では扱わない記号に込められた「意味」を読み取るのは
現状では人間にしかできない

機械が得意なことは機械に任せて
人間は人間にしかできないことに力を入れる方が得策だろう