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

実用化

[kuramori (38110)]

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

Re:実用化

[SteppingWind (2654)]

適当なアプリケーションを作成するのに理論を理解することが不要であること.

Re:実用化

[fcp (32783)]

適当なアプリケーションを作成するのに理論を理解することが不要であること.

それは普及する原因ではなく普及した結果でしょう。 ML が普及していて、まだ C 言語が普及していない夢の世界では、「ポインター演算の理論が難しい」などと言われていそうな気がします。

Re:実用化

[SteppingWind (2654)]

ML が普及していて、まだ C 言語が普及していない夢の世界では、「ポインター演算の理論が難しい」などと言われていそうな気がします。

そんな高度なことを要求されても困ります.

業務システムでのエンドプログラマのレベルは

• 関数/サブルーチンの概念が無い(出来合いの関数/サブルーチンは言語の命令として捉えている)
• 配列以外のデータ構造の概念が無い
• 名前空間の概念が無い(名前が同じなら実体も同じ)

という具合で, 抽象的な思考は一切出来ないという前提で評価しないと, 言語の実用性は判断できません. そういう意味ではC言語でさえ実用的には難しすぎて, 今日での業務プログラムでは以前のアセンブリ言語と同じく, 速度やシステムの直接呼び出しが必要となる局面でもなければ使われることは少なくなりました.

Re:実用化

[fcp (32783)]

興味深いお話、ありがとうございます。 #1795494 [srad.jp] で書いたポインター演算というのが高度過ぎて例として適切でないなら、「ポインター演算の理論が難しい」と書いた部分を「破壊的代入の理論が難しい」とでも置き換えてください。 #1795494 の論旨は変わりません。

Re:実用化

[IdentifiedCoward (20520)]

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

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

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

Re:実用化

[the.ACount (31144)]

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

--
the.ACount

Re:

[Anonymous Coward]

べつに完璧な証明を与える必要はありませんが。証明したい部分だけでOKですよ。

どうしてこう極端なんだろ。

Re:実用化

[IdentifiedCoward (20520)]

一部分についても、その厳密な証明はたぶん大変でしょうし、
証明しなかった部分は、当然不具合が残る可能性がありますよ。

普通の開発においても、障害が出るのはもともとテストや考慮が不十分だった部分の場合も
多いですし。

Re:

[Anonymous Coward]

> 証明しなかった部分は、当然不具合が残る可能性がありますよ。

ありますが、何か問題でも？

それでも従来のプログラミング言語よりはバグは少なくなるでしょう。それで満足できないのですか？
本質的には強い型付けやコントラクトやアサーションとかわるものではありません。あれらはバグを完全になくすためのものではありませんが、十分役に立っていますよね？

Re:実用化

[IdentifiedCoward (20520)]

程度にもよりますが、バグを少なくするためには、coqのような定理証明支援システムを導入するよりも、
他の方法を実践するほうが、より現実的だというのが私の感想です。
たとえば、より強い型付けの強い言語であれば、コンパイルするだけで異常を発見できるでしょうし、
コントラクトやアサーションは適切なテストケースにより、実行時エラーとして異常を発見することができるでしょう。

しかし、定理証明支援システムを部分的にでも導入するのであれば、それが部分的であろうとも、
理論に基づいた厳密な証明が必要とされます。

その厳密さが手間であり、部分的な正しさが検証できれば良いというのではあれば、強い型付けやコントラクトやアサーションの
ほうが、一般的に手軽なのではないかと考えます。

もちろん、すべての状況にあてはまるわけではないでしょうから、
役に立つとお考えであれば、定理証明支援システムをご利用されてはいかがでしょうか。

Re:

[Anonymous Coward]

一体何の話をなさってるのでしょうか。

証明主導でプログラムを書くのはたしかに頭の切り替えが必要ですが、(それでも関数型言語へのシフトを考えればもう一歩踏み出す程度でしょう)
依存型をちょっと使うことすら手間だと考えておられるのが不思議でなりません。

Re:実用化

[IdentifiedCoward (20520)]

現在広く使われているプログラミング言語から、関数型言語へのシフトをはじめとして、
依存型主導でのプログラムの導出や証明について、
一部の人たちを除いて、世の中の多くのプログラマが実践できることではないと考えます。

旧世代のプログラミング言語しか利用しない開発者や、
プログラミング言語自体を理解しない方たちがいるこの業界において、
これが手間でないとか、手間と考えるのが不思議でならないというのは、現実的でないと思います。

もちろん、特定の領域においては、実用の余地があると思いますが。

Re:

[Anonymous Coward]

オブジェクト指向のときも同じことを言われていたので同意できませんが、見解の相違の源が明らかになったのでよしとしましょう。

Re:実用化

[fcp (32783)]

依存型を持つプログラミング言語は、勉強してみようと思って Agda のチュートリアル [chalmers.se]を読み始めてはいるものの、まだ自分で触ってみたことはありません。

証明主導でプログラムを書くのはたしかに頭の切り替えが必要ですが、(それでも関数型言語へのシフトを考えればもう一歩踏み出す程度でしょう)
依存型をちょっと使うことすら手間だと考えておられるのが不思議でなりません。

証明主導でプログラムを書かずに「依存型をちょっと使う」というのが想像できずにいるのですが、特に依存型を使いたい部分だけ使って、大部分は普通に ML や Haskell のようにプログラムを書くというのは可能なのでしょうか。

Re:

[Anonymous Coward]

たとえば、行列の行数や列数を型に含めることができますので、行列の乗算などジェネリックな関数を安全に書くことができます。
型推論は処理系がやってくれます。
Agdaはいろいろ面倒なところもありますが、ATSのほうは比較的すぐ使えると思います。
http://www.ats-lang.org/ [ats-lang.org]

逆に、「スタックに値をプッシュしてポップするとスタックと値が元に戻る」という証明を型で書く時は、頭を切り替える必要がありますね。
証明自体は簡単ですが、確かに慣れないと雲をつかむようなところがあると思います。

破壊的代入に慣れた人が、関数的プログラミングをするときは最初は戸惑うと思いますが、それと似た感覚ではないでしょうか。私の場合はそうです。

Re:実用化

[fcp (32783)]

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 の方が入りやすそうなので、そちらを先に見てみたいと思います。

Re:実用化

[SteppingWind (2654)]

証明を与えるって, どんな人ならできるんですか? 経理とか生産管理をしている人はできるんですか?

Re:

[Anonymous Coward]

適切なエラーメッセージを出せるようにすることかも