正しさの証明

日本語はコンパイラによる静的チェックができない

 Wordとか使えば日本語の表現の誤りは警告してくれるかもしれないが、その日本語が表現するプログラムが正しいかは分からない。

日本語でプログラミングしてはいけない理由 - プログラマーの脳みそ

に対するツッコミだと思うけども、

id:eldesh
ネタにマジレスかもしれませんが,
プログラム言語でも静的なチェックでは,表現するプログラムが正しいかは(現実的な規模のコードではほとんど)確認できませんよね.

2010-01-08 - プログラマーの脳みそ

はなかなか鋭い。表現の揚げ足をとられちゃったなあ、と思いつつ

id:Nagise
プログラム言語の静的なチェックで、表現するプログラムの明らかな誤りは現実的な規模のコードでも100%検出できますよ :-)

2010-01-08 - プログラマーの脳みそ

と詭弁をろうしてみた。

程度問題

 正しいことを証明することと、誤りがあることを証明することの違い。これは悪魔の証明というやつだ。

 日本語でもプログラム言語でも、誤りが無いことの証明はとても難しい。対して誤りがあることの証明は誤りの実例をもってすれば足りる。プログラム言語の静的チェックでは型の取り違えとか、バグパターンとかを容易に検出することができる*1

 もっとも、現在の技術レベルだと日本語でも敬体と常体が混ざっているだとか、用語の表現のブレだとかは静的に解析して警告してくれるぐらいにはなっているんだけどね。

 プログラム言語のうち動的言語であっても、明らかに誤りというものは警告できる時代だ。それどころか、日本語という自然言語ですら明らかな誤りを警告できてしまう。じゃあ静的型付けの言語のアドバンテージがないかというとそういうわけじゃない。

 どのようなケースの誤りを検出出来るか、と言った場合により多くの誤りを検出できるのはいわゆる静的型付けの言語である。誤り検出を出来るか、出来ないかの二択で考えると日本語を含め多くの自然言語も「検出できる」となってしまうだろう。

 そして、「正しさの証明」ということが出来るか、出来ないかという二択で考えると、Javaだろうが日本語だろうがみな「出来ない」になってしまうだろう。

*1:JavaならばEclipseプラグインFindbugsを用いるとバグパターン検出ができる