[ アカウントをゲット！ ]
リンク先より
>仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。
仕様も考えず、アイディアだけ思いついて、面白い部分コア部分から作り始めてグダグダのうちに何とか動くものを作る
->デバッグにつぐデバッグ、拡張に次ぐ拡張でコードはプログラマの管理能力を超えるまでにカオス化。
->半年～数年放って置かれる
->全面的にリライト。細部から全体にいたるまで問題点の俯瞰的な理解を得た今、すばらしくすっきりしたコードが書ける。
->完成
という道をたどるのがプログラミングの楽しさ、醍醐味じゃないか。
え？趣味のプログラミングはそれでよいかもしれないが、仕事で作られるプログラムはそれじゃだめだろうって。はっはっは、何言ってんですか。プログラミングなんて仕事にするもんじゃないですよ。
コメントを書く
嫌なら使わなければいいのに・・・
はっ！なるほど、饅頭怖いの人か。（今風にはツンデレって言うんだっけ？）
親コメント
いろいろ良さ気な感じに聞こえますが、次のような機能はないんでしょうか？・営業が短納期で受注するのを防ぐ機能・仕様が固まるのにかかって遅れた時間の分だけ納期をのばす機能
この辺の機能が実装されれば間違いなくブレイクすると思います。
Agdaと聞いて、即完顔阿骨打を連想した俺はエロマンガ脳＃いや好きではないんだが
Agda言語で書かれたプログラムは世界で一番優れたプログラムだ！私は今までに一度も間違ったことのないプログラマだ！
♪世界で一番すぐれた言語♪♪命令絶対 規則はいっぱい♪
ルチ将軍万歳！
プログラムは書いた通りにしか動かない
プログラムは書いたとおりにしか動かないんだから書いた人間より高度な検証はできないという意味でしょうか。そうですね、Bonanzaの作者が駒の動かし方くらいしか知らないなんてことはあるはずがないし、ベイジアンフィルタは人間様が考え抜いたフィルタルールに勝てるはずがないし、遺伝的アルゴリズムの研究なんてものは詐欺の塊ですよね。まあ万物の霊長が0と1の羅列ごときに負けるはずがないと思いたい気持ちはよく分かりますが。
貴方は元コメが書いていないことに嚙み付いているが、そんな事をしても意義は無い。
まず書いてあるとおりに文章を読む能力を身に着けることから始めよう。万物の霊長を自称したり他人を揶揄するのはそれからでも遅くないよ。
プログラムは書いたとおりにしか動かないんだから書いた人間より高度な検証はできないという意味でしょうか。
誰もそんなことは言っていない。書いたとおりに動くからと言って、その出力を人間が予測できるわけではない。そもそも出力が予測できるのであればコンピュータは要らない。
＞万物の霊長が0と1の羅列ごときに負けるはずがないA、T、G、Cのバリエーション舐めんな
人間は書いたとおりに読まないのにね。
人間は考えた通りに書くことも出来ないんだよね。
逆じゃないですかね。形式仕様言語とか詳しくはないですが、詳しい人の話を伺っている限りでは、「動かないように書く」ことをいかに防ぐか？ という話のようですが。
書いたようにすら動かないコンピュータの話なんか、誰もしてませんよ？
C言語にBlocks拡張 [ascii.jp]を入れれば多少は関数型言語っぽくなる。
定数型ですべて解決
answer = 42
要件があやふやだったとか、仕様の詰めが甘いとか、入力されるデータを全部想定できてなかったとか、ミドルウェア・ＤＢ等の挙動を理解していなかったとか、そういうのが後々禍根を残すようなバグの原因だと思うのですが・・・。
で、そんなのは防げるんでしょうか。
どっちかというと、「要件があやふやだったり、仕様の詰めが甘かったり、入力されるデータを全部想定できてなかったり」したらプログラムが書けない、という方向が近い気がします。
ミドルウェア、DB等の挙動についても、原理的には、それらのインタフェース仕様が当該言語で与えられている場合、挙動を理解せずに書くと仕様の整合性がとれてないと怒られる、といった感じだと思うんですが、実際にAgdaみたいな言語から一般的なDBが叩けるレイヤが提供されているのかどうかは知りません。
もちろん、本来の要件に対して間違ったモデル化をして仕様定義してしまう、というバグについてはいかんともしがたいでしょう。
そうすると「矛盾があることをないことにする」機能が言語に必要になって、そういう部分をモジュールにまとめることで将来的なトラブル要素を一括して管理できる矛盾管理モジュールが生まれることになります。
・・・これはこれで価値あるかも？
> バグのないプログラム開発に興味のあるみなさんも参加してみてはいかがでしょうか
本当に「バグのないプログラム開発」なんて絵空事が実現できるなら参加してみたいかもｗだって、仕様書にバグがあった場合とか、仕様書を読む人間の理解度不足による実装ミス(バグ)はどんな言語を使っても回避不可能でしょ。＜多くのバグの発生箇所ってここでしょw基本的にプログラムは書いた通りにしか動かないわけだし。また、勝手にコンパイラやリンカに書き換えられても迷惑だしなｗ ＜最適化とかでも酷い目にあうのにｗ
> Hello World程度でバグを入れるのってかなり難しいと思う。
それは、非常に上手に作られたprintf関数なりなんなりが既に用意してあるから。まず、どこまでが「バグがない」と仮定できる範囲なのか示さないと。
> どうしてこう万能でなければ役立たずだと思いたがるんでしょうかねえ
別に万能である必要は無いんだよ。ただ、万能をうたっているモノに良いものなしなのが問題。＜人目を引きたいのは理解できるけどね。「バグの無いプログラム環境」ってうたい文句なら、バグが発生した時点でダメダメな環境なわけでｗ誇大広告甚だしいって思ってしまう。
こんなケース（開発）に向いているって言語なら、釣り！？なんていわない。もしくは、簡単（ガワだけでも）に書けるってな話ならなんら不思議では無いしね。
>「これこれなので、バグが減ります」という説明は、プログラムに素人な経営者に> 受けが良いので、新しい言語を売り込もうとした時、いつも（何十年も）使われている、> 売り文句ですね。
御意。ただ、この売り文句が似非くささを醸し出す原因なのに、何処も止めないんだよねぇ～。＜またかと思ってしまう。
そうかなぁ、同じモノを同じスキルの人が作るなら新しい言語と古い言語のバグは雲泥の差があると思うけど
時代の変化で作る対象が複雑化していたり技術の普及でボンクラ高度なスキルを持たない人でもプログラミングするようになってるけどそれを言語を測る物差しで一緒に測ってない？
将軍「バグのないプログラムを作ってみせよ」一休「ではバグのない仕様書を出してください」
悪いことに「バグのない仕様書」も, ほっておけば腐ってウジがわきますから.
永遠不滅の聖杯のごとき仕様書を持ってこないと駄目ですね.
「形式手法」こそが曖昧さのない「仕様」を書くことと等価だ、とかなんとか言ってみる。
不完全性原理をAgdaに移植できないんだろうか。
x < 120匹潰すとgenocide状態でもう出現しなくなるんだって．まめちしきだよ．
やっとこさ青いバグを潰しきったと思ったら、今度は赤いバグに襲われたんです！いったいどうすればいいでしょうか？
黄色いバグで一掃だ～♪
このページのすべての商標と著作権はそれぞれの所有者が有します。 コメントやユーザ日記に関しては投稿者が有します。 のこりのものは、© 2001-2010 OSDN です。
なんてことをするんだ (スコア:4, おもしろおかしい)
リンク先より
>仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。
仕様も考えず、アイディアだけ思いついて、面白い部分コア部分から作り始めてグダグダのうちに
何とか動くものを作る
->デバッグにつぐデバッグ、拡張に次ぐ拡張でコードはプログラマの管理能力を超えるまでにカオス化。
->半年～数年放って置かれる
->全面的にリライト。細部から全体にいたるまで問題点の俯瞰的な理解を得た今、
すばらしくすっきりしたコードが書ける。
->完成
という道をたどるのがプログラミングの楽しさ、醍醐味じゃないか。
え？趣味のプログラミングはそれでよいかもしれないが、
仕事で作られるプログラムはそれじゃだめだろうって。
はっはっは、何言ってんですか。プログラミングなんて仕事にするもんじゃないですよ。
コメントを書く
Re:なんてことをするんだ (スコア:1, すばらしい洞察)
嫌なら使わなければいいのに・・・
はっ！なるほど、饅頭怖いの人か。（今風にはツンデレって言うんだっけ？）
コメントを書く
親コメント
Re:なんてことをするんだ (スコア:1, 参考になる)
コメントを書く
親コメント
Re:なんてことをするんだ (スコア:4, おもしろおかしい)
いろいろ良さ気な感じに聞こえますが、次のような機能はないんでしょうか？
・営業が短納期で受注するのを防ぐ機能
・仕様が固まるのにかかって遅れた時間の分だけ納期をのばす機能
この辺の機能が実装されれば間違いなくブレイクすると思います。
◆IZUMI162i6 [mailto]
Free or not Free, that is the question.
コメントを書く
親コメント
名前の由来は (スコア:2)
それとも Anti GuDA guda ですかね。
コメントを書く
Re:名前の由来は (スコア:1, おもしろおかしい)
Agdaと聞いて、即完顔阿骨打を連想した俺はエロマンガ脳
＃いや好きではないんだが
コメントを書く
親コメント
Re:名前の由来は (スコア:0)
コメントを書く
親コメント
Re:名前の由来は (スコア:0)
コメントを書く
親コメント
Re:名前の由来は (スコア:1, すばらしい洞察)
Agda言語で書かれたプログラムは世界で一番優れたプログラムだ！
私は今までに一度も間違ったことのないプログラマだ！
♪世界で一番すぐれた言語♪
♪命令絶対 規則はいっぱい♪
ルチ将軍万歳！
コメントを書く
親コメント
Re:名前の由来は (スコア:0)
コメントを書く
親コメント
どんな言語を使おうが (スコア:2)
プログラムは書いた通りにしか動かない
コメントを書く
教え方による (スコア:-1, フレームのもと)
プログラムは書いたとおりにしか動かないんだから書いた人間より高度な検証はできないという意味でしょうか。
そうですね、Bonanzaの作者が駒の動かし方くらいしか知らないなんてことはあるはずがないし、ベイジアンフィルタは人間様が考え抜いたフィルタルールに勝てるはずがないし、遺伝的アルゴリズムの研究なんてものは詐欺の塊ですよね。
まあ万物の霊長が0と1の羅列ごときに負けるはずがないと思いたい気持ちはよく分かりますが。
コメントを書く
親コメント
Re:教え方による (スコア:0)
貴方は元コメが書いていないことに嚙み付いているが、そんな事をしても意義は無い。
まず書いてあるとおりに文章を読む能力を身に着けることから始めよう。
万物の霊長を自称したり他人を揶揄するのはそれからでも遅くないよ。
コメントを書く
親コメント
Re:教え方による (スコア:0)
誰もそんなことは言っていない。書いたとおりに動くからと言って、その出力を人間が予測できるわけではない。そもそも出力が予測できるのであればコンピュータは要らない。
コメントを書く
親コメント
「教え方による」というのは同意だけど (スコア:4, おもしろおかしい)
＞万物の霊長が0と1の羅列ごときに負けるはずがない
A、T、G、Cのバリエーション舐めんな
コメントを書く
親コメント
Re:教え方による (スコア:2, おもしろおかしい)
人間は書いたとおりに読まないのにね。
◆IZUMI162i6 [mailto]
Free or not Free, that is the question.
コメントを書く
親コメント
Re:教え方による (スコア:1)
人間は考えた通りに書くことも出来ないんだよね。
コメントを書く
親コメント
Re:教え方による (スコア:0)
コメントを書く
親コメント
Re:どんな言語を使おうが (スコア:0)
逆じゃないですかね。
形式仕様言語とか詳しくはないですが、詳しい人の話を伺っている限りでは、「動かないように書く」ことをいかに防ぐか？ という話のようですが。
書いたようにすら動かないコンピュータの話なんか、誰もしてませんよ？
コメントを書く
親コメント
Re:どんな言語を使おうが (スコア:0)
「思わなかったことが書かれれば、すぐ目に付く」言語なら「思ったことが書けている」可能性が上がり、
すなわち、「思ったとおりに動く。」
コメントを書く
親コメント
また関数か (スコア:0)
コメントを書く
Re:また関数か (スコア:0)
コメントを書く
親コメント
Re:また関数か (スコア:0)
C言語にBlocks拡張 [ascii.jp]を入れれば多少は関数型言語っぽくなる。
コメントを書く
親コメント
Re:また関数か (スコア:0)
定数型ですべて解決
answer = 42
コメントを書く
親コメント
どちらかというと (スコア:1)
要件があやふやだったとか、仕様の詰めが甘いとか、入力されるデータを全部想定できてなかったとか、ミドルウェア・ＤＢ等の挙動を理解していなかったとか、そういうのが後々禍根を残すようなバグの原因だと思うのですが・・・。
で、そんなのは防げるんでしょうか。
神社でC#.NET
コメントを書く
Re:どちらかというと (スコア:2, 興味深い)
どっちかというと、「要件があやふやだったり、仕様の詰めが甘かったり、入力されるデータを全部想定できてなかったり」したらプログラムが書けない、という方向が近い気がします。
ミドルウェア、DB等の挙動についても、原理的には、それらのインタフェース仕様が当該言語で与えられている場合、挙動を理解せずに書くと仕様の整合性がとれてないと怒られる、といった感じだと思うんですが、実際にAgdaみたいな言語から一般的なDBが叩けるレイヤが提供されているのかどうかは知りません。
もちろん、本来の要件に対して間違ったモデル化をして仕様定義してしまう、というバグについてはいかんともしがたいでしょう。
コメントを書く
親コメント
Re:どちらかというと (スコア:0)
その延長として要求自体に問題があることも証明可能かもしれませんね。
そうなるとこんな会話が行われることになると。
「先日頂いたお客様の社内ルールを形式言語で記述して見たところ矛盾があるようです」
「我が社はずっとこのやり方でやってきて問題は無かった、そんな言い訳は許さない」
「では見逃している業務処理があるのだと思います、調べて頂けないでしょうか？」
「これまでもシステム化していないだけで、社内ルールを厳守してきた。問題ない」
「ですから矛盾がですね」
(以下略)
コメントを書く
親コメント
Re:どちらかというと (スコア:0)
そうすると「矛盾があることをないことにする」機能が言語に必要になって、
そういう部分をモジュールにまとめることで将来的なトラブル要素を一括して
管理できる矛盾管理モジュールが生まれることになります。
・・・これはこれで価値あるかも？
コメントを書く
親コメント
釣り！？ (スコア:1)
> バグのないプログラム開発に興味のあるみなさんも参加してみてはいかがでしょうか
本当に「バグのないプログラム開発」なんて絵空事が実現できるなら参加してみたいかもｗ
だって、仕様書にバグがあった場合とか、仕様書を読む人間の理解度不足による実装ミス(バグ)
はどんな言語を使っても回避不可能でしょ。＜多くのバグの発生箇所ってここでしょw
基本的にプログラムは書いた通りにしか動かないわけだし。
また、勝手にコンパイラやリンカに書き換えられても迷惑だしなｗ
＜最適化とかでも酷い目にあうのにｗ
コメントを書く
Re:釣り！？ (スコア:0)
コメントを書く
親コメント
Re:釣り！？ (スコア:0)
(デバッグしてないってのは論外だが)
そこで気付くのはバグの有無の境界線。
そんな分岐点が見えていないんでしょ、スレ元は。
何でもかんでもバグ付きと思ってるようだから。
コメントを書く
親コメント
Re:釣り！？ (スコア:1)
> Hello World程度でバグを入れるのってかなり難しいと思う。
それは、非常に上手に作られたprintf関数なりなんなりが既に用意してあるから。
まず、どこまでが「バグがない」と仮定できる範囲なのか示さないと。
1を聞いて0を知れ!
コメントを書く
親コメント
Re:釣り！？ (スコア:1)
> どうしてこう万能でなければ役立たずだと思いたがるんでしょうかねえ
別に万能である必要は無いんだよ。
ただ、万能をうたっているモノに良いものなしなのが問題。＜人目を引きたいのは理解できるけどね。
「バグの無いプログラム環境」ってうたい文句なら、バグが発生した時点でダメダメな環境なわけでｗ
誇大広告甚だしいって思ってしまう。
こんなケース（開発）に向いているって言語なら、釣り！？なんていわない。
もしくは、簡単（ガワだけでも）に書けるってな話ならなんら不思議では無いしね。
コメントを書く
親コメント
Re:釣り！？ (スコア:1, すばらしい洞察)
コメントを書く
親コメント
Re:釣り！？ (スコア:1)
「これこれなので、バグが減ります」という説明は、プログラムに素人な経営者に
受けが良いので、新しい言語を売り込もうとした時、いつも（何十年も）使われている、
売り文句ですね。
まあその辺は、例えばセミナーへの出張を申請する際に、適当に引用する程度にして
こういう新しい言語は、頭の体操だと思えば、なかなか面白いです。
コメントを書く
親コメント
Re:釣り！？ (スコア:1)
>「これこれなので、バグが減ります」という説明は、プログラムに素人な経営者に
> 受けが良いので、新しい言語を売り込もうとした時、いつも（何十年も）使われている、
> 売り文句ですね。
御意。
ただ、この売り文句が似非くささを醸し出す原因なのに、
何処も止めないんだよねぇ～。＜またかと思ってしまう。
コメントを書く
親コメント
Re:釣り！？ (スコア:0)
そうかなぁ、同じモノを同じスキルの人が作るなら
新しい言語と古い言語のバグは雲泥の差があると思うけど
時代の変化で作る対象が複雑化していたり
技術の普及で
ボンクラ高度なスキルを持たない人でもプログラミングするようになってるけどそれを言語を測る物差しで一緒に測ってない？
コメントを書く
親コメント
それ以前に (スコア:1, 興味深い)
＞ バグのないプログラム開発
の産物なのだろうか？
コメントを書く
親コメント
Re:それ以前に (スコア:0)
(1) 人力で正当性が検証できる程度の、当該言語の極めて小さなサブセットのコンパイラを開発
(2) (1)のサブセットのコンパイラを使って、フルセットのコンパイラを記述
(3) (2)自身を(2)で書き直し
とやれば、「記述されたソースと言語仕様の範囲内で確実に一致する挙動を示す実行ファイルが作成されること」は保証できますね。
コメントを書く
親コメント
Re:釣り！？ (スコア:5, おもしろおかしい)
将軍「バグのないプログラムを作ってみせよ」
一休「ではバグのない仕様書を出してください」
コメントを書く
親コメント
Re:釣り！？ (スコア:1)
悪いことに「バグのない仕様書」も, ほっておけば腐ってウジがわきますから.
永遠不滅の聖杯のごとき仕様書を持ってこないと駄目ですね.
コメントを書く
親コメント
それは仕様です。 (スコア:0)
つまり、「バグのないプログラム開発｣が可能だということです。
コメントを書く
親コメント
というか (スコア:0)
「形式手法」こそが曖昧さのない「仕様」を書くことと等価だ、とかなんとか言ってみる。
コメントを書く
親コメント
Re:というか (スコア:1)
不完全性原理をAgdaに移植できないんだろうか。
1を聞いて0を知れ!
コメントを書く
親コメント
バグのないプログラム (スコア:0)
x < 120匹潰すとgenocide状態でもう出現しなくなるんだって．まめちしきだよ．
コメントを書く
Re:バグのないプログラム (スコア:0)
やっとこさ青いバグを潰しきったと思ったら、今度は赤いバグに襲われたんです！
いったいどうすればいいでしょうか？
コメントを書く
親コメント
Re:バグのないプログラム (スコア:2)
黄色いバグで一掃だ～♪
コメントを書く
親コメント
物は言いよう (スコア:1)
出来上がったプログラムそのものにバグが無いと言っているわけじゃないんですよね？
＃仕様の時点でバグっているものをどうやってバグ無しで作れと
コメントを書く
Re:物は言いよう (スコア:0)
そういう意味では、バグという用語を不用意に用いるのはよくないですね。
コメントを書く
親コメント
時期的にも、 (スコア:0)
コメントを書く