アカウント名:
パスワード:
こういう理論に基づいた言語が普及するためにはなにが必要なのだろう？C言語で書かれたライブラリを簡単に呼び出せること？IDEがあること？GUIが簡単に作れること？JVM上で動くこと？ブラウザで動くこと？Apple,Microsoftが発売する／Googleが使っているとばれること？
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
「科学者は100%安全だと保証できないものは動かしてはならない」、科学者「えっ」、プログラマ「えっ」
実用化 (スコア:1)
こういう理論に基づいた言語が普及するためにはなにが必要なのだろう？
C言語で書かれたライブラリを簡単に呼び出せること？
IDEがあること？
GUIが簡単に作れること？
JVM上で動くこと？
ブラウザで動くこと？
Apple,Microsoftが発売する／Googleが使っているとばれること？
Re: (スコア:1)
そもそも、証明すべき性質を形式的に定義する事自体も、専門的で複雑な作業だから、普及しない。
日本語などの自然言語で仕様書を書いたり、プログラムのテスト仕様を作成する人が、
coqで使われているような理論を理解すれば、自分たちの作業が、理論的な厳密さから
いかにかけ離れているのかということが理解できると思う。
実用的な立場からいえば、多少の不具合やあいまいさがあっても、現実的な作業量で充分役に立つソフトウェアが開発できれば、
それでよいとも考えられる。
Re: (スコア:0)
どうしてこう極端なんだろ。
Re: (スコア:1)
証明しなかった部分は、当然不具合が残る可能性がありますよ。
普通の開発においても、障害が出るのはもともとテストや考慮が不十分だった部分の場合も
多いですし。
Re: (スコア:0)
ありますが、何か問題でも？
それでも従来のプログラミング言語よりはバグは少なくなるでしょう。それで満足できないのですか？
本質的には強い型付けやコントラクトやアサーションとかわるものではありません。あれらはバグを完全になくすためのものではありませんが、十分役に立っていますよね？
Re: (スコア:1)
他の方法を実践するほうが、より現実的だというのが私の感想です。
たとえば、より強い型付けの強い言語であれば、コンパイルするだけで異常を発見できるでしょうし、
コントラクトやアサーションは適切なテストケースにより、実行時エラーとして異常を発見することができるでしょう。
しかし、定理証明支援システムを部分的にでも導入するのであれば、それが部分的であろうとも、
理論に基づいた厳密な証明が必要とされます。
その厳密さが手間であり、部分的な正しさが検証できれば良いというのではあれば、強い型付けやコントラクトやアサーションの
ほうが、一般的に手軽なのではないかと考えます。
もちろん、すべての状況にあてはまるわけではないでしょうから、
役に立つとお考えであれば、定理証明支援システムをご利用されてはいかがでしょうか。
Re: (スコア:0)
証明主導でプログラムを書くのはたしかに頭の切り替えが必要ですが、(それでも関数型言語へのシフトを考えればもう一歩踏み出す程度でしょう)
依存型をちょっと使うことすら手間だと考えておられるのが不思議でなりません。
Re: (スコア:2, 興味深い)
依存型主導でのプログラムの導出や証明について、
一部の人たちを除いて、世の中の多くのプログラマが実践できることではないと考えます。
旧世代のプログラミング言語しか利用しない開発者や、
プログラミング言語自体を理解しない方たちがいるこの業界において、
これが手間でないとか、手間と考えるのが不思議でならないというのは、現実的でないと思います。
もちろん、特定の領域においては、実用の余地があると思いますが。
Re:実用化 (スコア:0)