スラッシュドット・ジャパン

リンク先より

>仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。

仕様も考えず、アイディアだけ思いついて、面白い部分コア部分から作り始めてグダグダのうちに
何とか動くものを作る

->デバッグにつぐデバッグ、拡張に次ぐ拡張でコードはプログラマの管理能力を超えるまでにカオス化。

->半年～数年放って置かれる

->全面的にリライト。細部から全体にいたるまで問題点の俯瞰的な理解を得た今、
すばらしくすっきりしたコードが書ける。

->完成

という道をたどるのがプログラミングの楽しさ、醍醐味じゃないか。

え？趣味のプログラミングはそれでよいかもしれないが、
仕事で作られるプログラムはそれじゃだめだろうって。
はっはっは、何言ってんですか。プログラミングなんて仕事にするもんじゃないですよ。

私はしきい値を３に設定し、すば洞や参考になるは＋１になるようにして普段見ているが、
おもしろおかしいモデだけしか出てこないストーリーは初めてかも知れない。

おもしろおかしいは１モデ程度のものは面白おかしくないものが多いので、＋補正はしていないのだが。

プログラムは書いた通りにしか動かない

3種類ぐらいの大分類に分かれる仕様記述言語において、Agdaは仕様の形式検証に重点が置かれているタイプ。
普通なら何十パターンかのテストパターンを与えて、ブラックボックステストも十分時間をかけて行いようやく発見できるかどうかという類のバグが
検証器を通せばぴたりとわかるのはすばらしい(シークエント計算なんて全くついて行けてないがチュートリアルhttp://unit.aist.go.jp/cvs/Agda/main.pdf [aist.go.jp]p.54とかあとagdaでググったり)

もっとも、ソフトウエアの論理の妥当性を形式検証しようという企ては歴史がかなり古いはずなのに
未だ現場プログラマーから冷淡な視線を浴びせられ続ける現実がこの分野の袋小路寸前の困難さを表しているのかも(汗

ただし、型関連の記述ミスをビルド一発で白黒つけられるという強く型付けられた言語(CやC++やC#やJava、but not JavaScript)の特質も
形式検証技術の遠い親戚なはずで現場においても全く御利益を被っていないわけではない
…と思う

要件があやふやだったとか、仕様の詰めが甘いとか、入力されるデータを全部想定できてなかったとか、ミドルウェア・ＤＢ等の挙動を理解していなかったとか、そういうのが後々禍根を残すようなバグの原因だと思うのですが・・・。

で、そんなのは防げるんでしょうか。

> バグのないプログラム開発に興味のあるみなさんも参加してみてはいかがでしょうか

本当に「バグのないプログラム開発」なんて絵空事が実現できるなら参加してみたいかもｗ
だって、仕様書にバグがあった場合とか、仕様書を読む人間の理解度不足による実装ミス(バグ)
はどんな言語を使っても回避不可能でしょ。＜多くのバグの発生箇所ってここでしょw
基本的にプログラムは書いた通りにしか動かないわけだし。
また、勝手にコンパイラやリンカに書き換えられても迷惑だしなｗ　
＜最適化とかでも酷い目にあうのにｗ

黄色いバグで一掃だ～♪

関西型かよ！