>>205
>形式仕様を読み書きする時には、字面が持つ自然言語的意味を無視して
>あくまで記号操作の対象として扱う。
そんなことをは君（人間）は気にする必要はないのだ。
放っておいても証明器は完璧にそうしてくれる。
同じことを君（人間）がやってもそれこそ効果は半減する。

書くことは人間にしかできないのだが，そのとき「記号」で書いていては，
そもそもどういう対象を書いているかが分からないだろう？ｗ

>「形式的に」扱う訓練を受けていない人のために非形式的意味を使う。
訓練を受けているとかいないとかでなく、どんな相手だろうと、何を書いて
いるかを伝えるためには、単なる記号では伝わらないんだよ。

>非形式的な意味を持たせた時点で、その記述は形式仕様ではなくなる。
これも違う。人間がどういう読み方をしようと、machine readableであれば
形式仕様なんだよ。

あと、君が「形式手法を知らない人」「訓練を受けていない人」とよく
言ってるらしいのが気になるな。