アカウント名:
パスワード:
こういう理論に基づいた言語が普及するためにはなにが必要なのだろう？C言語で書かれたライブラリを簡単に呼び出せること？IDEがあること？GUIが簡単に作れること？JVM上で動くこと？ブラウザで動くこと？Apple,Microsoftが発売する／Googleが使っているとばれること？
依存型を持つプログラミング言語は、勉強してみようと思って Agda のチュートリアル [chalmers.se]を読み始めてはいるものの、まだ自分で触ってみたことはありません。
証明主導でプログラムを書くのはたしかに頭の切り替えが必要ですが、(それでも関数型言語へのシフトを考えればもう一歩踏み出す程度でしょう) 依存型をちょっと使うことすら手間だと考えておられるのが不思議でなりません。
証明主導でプログラムを書かずに「依存型をちょっと使う」というのが想像できずにいるのですが、特に依存型を使いたい部分だけ使って、大部分は普通に ML や Haskell のようにプログラムを書くというのは可能なのでしょうか。
たとえば、行列の行数や列数を型に含めることができますので、行列の乗算などジェネリックな関数を安全に書くことができます。型推論は処理系がやってくれます。Agdaはいろいろ面倒なところもありますが、ATSのほうは比較的すぐ使えると思います。http://www.ats-lang.org/ [ats-lang.org]
逆に、「スタックに値をプッシュしてポップするとスタックと値が元に戻る」という証明を型で書く時は、頭を切り替える必要がありますね。証明自体は簡単ですが、確かに慣れないと雲をつかむようなところがあると思います。
破壊的代入に慣れた人が、関数的プログラミングをするときは最初は戸惑うと思いますが、それと似た感覚ではないでしょうか。私の場合はそうです。
Agdaはいろいろ面倒なところもありますが、ATSのほうは比較的すぐ使えると思います。 http://www.ats-lang.org/ [ats-lang.org]
面白そうな言語の紹介、ありがとうございます。 ATS では
fun fact1 (x: int): int = if x > 0 then x * fact1 (x-1) else 1
が合法なのですね。 Agda では停止が保証されていない関数は定義できないので、素人目には、根本的に考え方が違うように思いました。 ATS の方が入りやすそうなので、そちらを先に見てみたいと思います。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
目玉の数さえ十分あれば、どんなバグも深刻ではない -- Eric Raymond
実用化 (スコア: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)
Re:実用化 (スコア:2)
依存型を持つプログラミング言語は、勉強してみようと思って Agda のチュートリアル [chalmers.se]を読み始めてはいるものの、まだ自分で触ってみたことはありません。
証明主導でプログラムを書かずに「依存型をちょっと使う」というのが想像できずにいるのですが、特に依存型を使いたい部分だけ使って、大部分は普通に ML や Haskell のようにプログラムを書くというのは可能なのでしょうか。
Re: (スコア:0)
たとえば、行列の行数や列数を型に含めることができますので、行列の乗算などジェネリックな関数を安全に書くことができます。
型推論は処理系がやってくれます。
Agdaはいろいろ面倒なところもありますが、ATSのほうは比較的すぐ使えると思います。
http://www.ats-lang.org/ [ats-lang.org]
逆に、「スタックに値をプッシュしてポップするとスタックと値が元に戻る」という証明を型で書く時は、頭を切り替える必要がありますね。
証明自体は簡単ですが、確かに慣れないと雲をつかむようなところがあると思います。
破壊的代入に慣れた人が、関数的プログラミングをするときは最初は戸惑うと思いますが、それと似た感覚ではないでしょうか。私の場合はそうです。
Re:実用化 (スコア:2)
面白そうな言語の紹介、ありがとうございます。 ATS では
が合法なのですね。 Agda では停止が保証されていない関数は定義できないので、素人目には、根本的に考え方が違うように思いました。 ATS の方が入りやすそうなので、そちらを先に見てみたいと思います。