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