「Coq 庵 - Coq プログラマのアンカンファレンス in 名古屋 (8/29)」記事へのコメント

実用化

[kuramori (38110)]

こういう理論に基づいた言語が普及するためにはなにが必要なのだろう？
C言語で書かれたライブラリを簡単に呼び出せること？
IDEがあること？
GUIが簡単に作れること？
JVM上で動くこと？
ブラウザで動くこと？
Apple,Microsoftが発売する／Googleが使っているとばれること？

Re:

[IdentifiedCoward (20520)]

実用的な複雑さのプログラムに対して、数学的に正しい証明を与えることは、とても大変な作業だし、
そもそも、証明すべき性質を形式的に定義する事自体も、専門的で複雑な作業だから、普及しない。

日本語などの自然言語で仕様書を書いたり、プログラムのテスト仕様を作成する人が、
coqで使われているような理論を理解すれば、自分たちの作業が、理論的な厳密さから
いかにかけ離れているのかということが理解できると思う。

実用的な立場からいえば、多少の不具合やあいまいさがあっても、現実的な作業量で充分役に立つソフトウェアが開発できれば、
それでよいとも考えられる。

Re:実用化

[the.ACount (31144)]

自分で書いたプログラムは可能なら部分的にでも証明するようにしてるが、皆はやってないのかな？
もちろん、証明したからといって正しいプログラムが保障されるわけじゃない。
証明命題自体が不適当な場合もあり、正しくても使えない場合もありでテストは必須だけど、試験実行では見つけられないバグを出すことができる。

--
the.ACount