[過去ﾛｸﾞ] 関数型プログラミング言語Haskell Part8 (994ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
952(4): デフォルトの名無しさん [sage] 2008/05/13(火)09:52
いくつか関数型言語を使う企業を見たり、経験しているが証明はまずしない。
定理証明支援系で証明できることはどうせたかが知れており、
これは業種にもよるので断言できないが、実際に保証したいことはまず
証明できない。できたとしても時間かかりすぎ。仕様が変更されれば
証明に要した労力も無駄。費用対効果の面から魅力を感じられない。
自動、半自動的な検証は当然大いに利用したいが、モデル検査はちょっと
おおげさ。やはり言語に付属している型検査、型推論が妥当な手段になる。
企業側が関数型言語を選ぶのにはいくつか理由があるが、結構重要視されて
いるのが、関数型言語を書ける人間を集める方が、Javaで集めるより、
当たりが多いという事実。もちろんそういう意味では機械証明ができる人材は
歓迎される。まあ、面接や2chのスレを見てる限り、これももうすぐ成り立た
なくなるだろうけど。
953: デフォルトの名無しさん [sage] 2008/05/13(火)16:05
>>952
> これは業種にもよるので断言できないが、
> 実際に保証したいことはまず証明できない。
まあ断言していいと思うよ。
955(1): デフォルトの名無しさん [sage] 2008/05/13(火)22:10
>>952
＞いくつか関数型言語を使う企業を見たり、経験しているが
可能ならば、具体例きぼんぬ。
956(2): デフォルトの名無しさん [sage] 2008/05/13(火)22:16
>>952
それは、計算機で数学の証明ができない、ということと等価なんでしょうか？
957(1): デフォルトの名無しさん [sage] 2008/05/13(火)22:17
>>952
実際にHaskellやOCamlを使っているところは、単純に静的型チェックによる安全性を重要視してるんじゃない？
Javaなんかも静的型チェックがあるけど、HaskellやOCamlはもっと安全で、でも、Javaほど冗長じゃない
っていうのが普通に便利だと思うけど。
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.034s