
関数型プログラミング言語「Agda」の研修コースを産総研が開催 75
ストーリー by hylom
ちょっと勉強したい 部門より
ちょっと勉強したい 部門より
あるAnonymous Coward 曰く、
産業技術総合研究所により、関数型プログラミング言語「Agda」の研修コースが開催されるそうです(産総研:システム検証研究センター:CVS研修コース「Agdaによる仕様記述」)。
Agdaは強力な依存型を備えた関数型プログラミング言語であり、証明支援システムとして利用できることでも知られています。また、その形式手法はプログラムの不具合を防ぐ開発手段として近年注目を集めています。
受講対象はAgdaに興味がある技術者、マネージャ、学生ということで、ある程度の開発経験があれば問題ないそうです。形式手法やバグのないプログラム開発に興味のあるみなさんも参加してみてはいかがでしょうか。
なんてことをするんだ (スコア:4, おもしろおかしい)
リンク先より
>仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。
仕様も考えず、アイディアだけ思いついて、面白い部分コア部分から作り始めてグダグダのうちに
何とか動くものを作る
->デバッグにつぐデバッグ、拡張に次ぐ拡張でコードはプログラマの管理能力を超えるまでにカオス化。
->半年~数年放って置かれる
->全面的にリライト。細部から全体にいたるまで問題点の俯瞰的な理解を得た今、
すばらしくすっきりしたコードが書ける。
->完成
という道をたどるのがプログラミングの楽しさ、醍醐味じゃないか。
え?趣味のプログラミングはそれでよいかもしれないが、
仕事で作られるプログラムはそれじゃだめだろうって。
はっはっは、何言ってんですか。プログラミングなんて仕事にするもんじゃないですよ。
Re:なんてことをするんだ (スコア:4, おもしろおかしい)
いろいろ良さ気な感じに聞こえますが、次のような機能はないんでしょうか?
・営業が短納期で受注するのを防ぐ機能
・仕様が固まるのにかかって遅れた時間の分だけ納期をのばす機能
この辺の機能が実装されれば間違いなくブレイクすると思います。
◆IZUMI162i6 [mailto]
Re:なんてことをするんだ (スコア:1, すばらしい洞察)
嫌なら使わなければいいのに・・・
はっ!なるほど、饅頭怖いの人か。(今風にはツンデレって言うんだっけ?)
Re:なんてことをするんだ (スコア:1, 参考になる)
おもしろおかしいばかりだ (スコア:4, おもしろおかしい)
私はしきい値を3に設定し、すば洞や参考になるは+1になるようにして普段見ているが、
おもしろおかしいモデだけしか出てこないストーリーは初めてかも知れない。
おもしろおかしいは1モデ程度のものは面白おかしくないものが多いので、+補正はしていないのだが。
名前の由来は (スコア:2)
それとも Anti GuDA guda ですかね。
Re:名前の由来は (スコア:1, おもしろおかしい)
Agdaと聞いて、即完顔阿骨打を連想した俺はエロマンガ脳
#いや好きではないんだが
Re: (スコア:0)
Re:名前の由来は (スコア:1, すばらしい洞察)
Agda言語で書かれたプログラムは世界で一番優れたプログラムだ!
私は今までに一度も間違ったことのないプログラマだ!
♪世界で一番すぐれた言語♪
♪命令絶対 規則はいっぱい♪
ルチ将軍万歳!
どんな言語を使おうが (スコア:2)
プログラムは書いた通りにしか動かない
Re: (スコア:0)
逆じゃないですかね。
形式仕様言語とか詳しくはないですが、詳しい人の話を伺っている限りでは、「動かないように書く」ことをいかに防ぐか? という話のようですが。
書いたようにすら動かないコンピュータの話なんか、誰もしてませんよ?
Re: (スコア:0)
「思わなかったことが書かれれば、すぐ目に付く」言語なら「思ったことが書けている」可能性が上がり、
すなわち、「思ったとおりに動く。」
「教え方による」というのは同意だけど (スコア:4, おもしろおかしい)
>万物の霊長が0と1の羅列ごときに負けるはずがない
A、T、G、Cのバリエーション舐めんな
Re:教え方による (スコア:2, おもしろおかしい)
人間は書いたとおりに読まないのにね。
◆IZUMI162i6 [mailto]
Re:教え方による (スコア:1)
人間は考えた通りに書くことも出来ないんだよね。
Re: (スコア:0)
貴方は元コメが書いていないことに嚙み付いているが、そんな事をしても意義は無い。
まず書いてあるとおりに文章を読む能力を身に着けることから始めよう。
万物の霊長を自称したり他人を揶揄するのはそれからでも遅くないよ。
Re: (スコア:0)
誰もそんなことは言っていない。書いたとおりに動くからと言って、その出力を人間が予測できるわけではない。そもそも出力が予測できるのであればコンピュータは要らない。
もっと目をキラキラさせるべき (スコア:2, 興味深い)
3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。
普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが
検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアルhttp://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)
もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史がかなり古いはずなのに
未だ現場プログラマーから冷淡な視線を浴びせられ続ける現実がこの分野の袋小路寸前の困難さを表しているのかも(汗
ただし、型関連の記述ミスをビルド一発で白黒つけられるという強く型付けられた言語(CやC++やC#やJava、but not JavaScript)の特質も
形式検証技術の遠い親戚なはずで現場においても全く御利益を被っていないわけではない
…と思う
Re: (スコア:0)
> 未だ現場プログラマーから冷淡な視線を浴びせられ続ける現実がこの分野の袋小路寸前の困難さを表しているのかも(汗
ハードウェアの世界では形式的検証は実用化されているのにねえ
なんでだろ
Re: (スコア:0)
至って明快な話でして。単に状態数が少ないからですよ。
どちらかというと (スコア:1)
要件があやふやだったとか、仕様の詰めが甘いとか、入力されるデータを全部想定できてなかったとか、ミドルウェア・DB等の挙動を理解していなかったとか、そういうのが後々禍根を残すようなバグの原因だと思うのですが・・・。
で、そんなのは防げるんでしょうか。
神社でC#.NET
Re:どちらかというと (スコア:2, 興味深い)
どっちかというと、「要件があやふやだったり、仕様の詰めが甘かったり、入力されるデータを全部想定できてなかったり」したらプログラムが書けない、という方向が近い気がします。
ミドルウェア、DB等の挙動についても、原理的には、それらのインタフェース仕様が当該言語で与えられている場合、挙動を理解せずに書くと仕様の整合性がとれてないと怒られる、といった感じだと思うんですが、実際にAgdaみたいな言語から一般的なDBが叩けるレイヤが提供されているのかどうかは知りません。
もちろん、本来の要件に対して間違ったモデル化をして仕様定義してしまう、というバグについてはいかんともしがたいでしょう。
釣り!? (スコア:1)
> バグのないプログラム開発に興味のあるみなさんも参加してみてはいかがでしょうか
本当に「バグのないプログラム開発」なんて絵空事が実現できるなら参加してみたいかもw
だって、仕様書にバグがあった場合とか、仕様書を読む人間の理解度不足による実装ミス(バグ)
はどんな言語を使っても回避不可能でしょ。<多くのバグの発生箇所ってここでしょw
基本的にプログラムは書いた通りにしか動かないわけだし。
また、勝手にコンパイラやリンカに書き換えられても迷惑だしなw
<最適化とかでも酷い目にあうのにw
Re:釣り!? (スコア:5, おもしろおかしい)
将軍「バグのないプログラムを作ってみせよ」
一休「ではバグのない仕様書を出してください」
Re:釣り!? (スコア:1)
悪いことに「バグのない仕様書」も, ほっておけば腐ってウジがわきますから.
永遠不滅の聖杯のごとき仕様書を持ってこないと駄目ですね.
Re:釣り!? (スコア:1)
「これこれなので、バグが減ります」という説明は、プログラムに素人な経営者に
受けが良いので、新しい言語を売り込もうとした時、いつも(何十年も)使われている、
売り文句ですね。
まあその辺は、例えばセミナーへの出張を申請する際に、適当に引用する程度にして
こういう新しい言語は、頭の体操だと思えば、なかなか面白いです。
Re:釣り!? (スコア:1)
>「これこれなので、バグが減ります」という説明は、プログラムに素人な経営者に
> 受けが良いので、新しい言語を売り込もうとした時、いつも(何十年も)使われている、
> 売り文句ですね。
御意。
ただ、この売り文句が似非くささを醸し出す原因なのに、
何処も止めないんだよねぇ~。<またかと思ってしまう。
Re: (スコア:0)
そうかなぁ、同じモノを同じスキルの人が作るなら
新しい言語と古い言語のバグは雲泥の差があると思うけど
時代の変化で作る対象が複雑化していたり
技術の普及で
ボンクラ高度なスキルを持たない人でもプログラミングするようになってるけどそれを言語を測る物差しで一緒に測ってない?
それ以前に (スコア:1, 興味深い)
> バグのないプログラム開発
の産物なのだろうか?
Re: (スコア:0)
Re:釣り!? (スコア:1)
> どうしてこう万能でなければ役立たずだと思いたがるんでしょうかねえ
別に万能である必要は無いんだよ。
ただ、万能をうたっているモノに良いものなしなのが問題。<人目を引きたいのは理解できるけどね。
「バグの無いプログラム環境」ってうたい文句なら、バグが発生した時点でダメダメな環境なわけでw
誇大広告甚だしいって思ってしまう。
こんなケース(開発)に向いているって言語なら、釣り!?なんていわない。
もしくは、簡単(ガワだけでも)に書けるってな話ならなんら不思議では無いしね。
Re:釣り!? (スコア:1, すばらしい洞察)
Re: (スコア:0)
(デバッグしてないってのは論外だが)
そこで気付くのはバグの有無の境界線。
そんな分岐点が見えていないんでしょ、スレ元は。
何でもかんでもバグ付きと思ってるようだから。
Re:釣り!? (スコア:1)
> Hello World程度でバグを入れるのってかなり難しいと思う。
それは、非常に上手に作られたprintf関数なりなんなりが既に用意してあるから。
まず、どこまでが「バグがない」と仮定できる範囲なのか示さないと。
1を聞いて0を知れ!
それは仕様です。 (スコア:0)
つまり、「バグのないプログラム開発」が可能だということです。
というか (スコア:0)
「形式手法」こそが曖昧さのない「仕様」を書くことと等価だ、とかなんとか言ってみる。
Re:というか (スコア:1)
不完全性原理をAgdaに移植できないんだろうか。
1を聞いて0を知れ!
物は言いよう (スコア:1)
出来上がったプログラムそのものにバグが無いと言っているわけじゃないんですよね?
#仕様の時点でバグっているものをどうやってバグ無しで作れと
Re: (スコア:0)
そういう意味では、バグという用語を不用意に用いるのはよくないですね。
また関数か (スコア:0)
Re: (スコア:0)
Re: (スコア:0)
C言語にBlocks拡張 [ascii.jp]を入れれば多少は関数型言語っぽくなる。
Re: (スコア:0)
定数型ですべて解決
answer = 42
バグのないプログラム (スコア:0)
x < 120匹潰すとgenocide状態でもう出現しなくなるんだって.まめちしきだよ.
Re: (スコア:0)
やっとこさ青いバグを潰しきったと思ったら、今度は赤いバグに襲われたんです!
いったいどうすればいいでしょうか?
Re:バグのないプログラム (スコア:2)
黄色いバグで一掃だ~♪
時期的にも、 (スコア:0)
関数型プログラミング言語「Ahoka」に見えた。 (スコア:0)
ただそれだけなのでAC
Re:関数型プログラミング言語「Ahoka」に見えた。 (スコア:1)
関西型かよ!
プログラミング言語以外の問題が大きい (スコア:0)
って事無いですか?
数年前にCOBOLでメインフレームのウォーターフォール・モデルのプロジェクトに参加した事があるけど、
意外と大過無く運営されてましたよ。