>>214
それが可能ならそれこそ形式仕様なぞ不要だな

そもそも何でも証明器で検証するのが前提になってる>>206は
形式手法にどんな夢を見ているんだ？

>>206
> 放っておいても証明器は完璧にそうしてくれる。
> 同じことを君（人間）がやってもそれこそ効果は半減する。

残念ながら証明器は放っておいても何もしてくれない。
証明器を有効に使うために必要なエフォートを知った上での
主張とは思えない。

> どんな相手だろうと、何を書いて
> いるかを伝えるためには、単なる記号では伝わらないんだよ。

piを「円周率」として読むレベルの厳密さで良いのであれば、
拘束文法による半形式仕様で十分だ。