「関数型プログラミング言語「Agda」の研修コースを産総研が開催」記事へのコメント

どちらかというと

[n_ayase (36873)]

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

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

--
神社でC#.NET

Re:どちらかというと

[Anonymous Coward]

どっちかというと、「要件があやふやだったり、仕様の詰めが甘かったり、入力されるデータを全部想定できてなかったり」したらプログラムが書けない、という方向が近い気がします。

ミドルウェア、DB等の挙動についても、原理的には、それらのインタフェース仕様が当該言語で与えられている場合、挙動を理解せずに書くと仕様の整合性がとれてないと怒られる、といった感じだと思うんですが、実際にAgdaみたいな言語から一般的なDBが叩けるレイヤが提供されているのかどうかは知りません。

もちろん、本来の要件に対して間違ったモデル化をして仕様定義してしまう、というバグについてはいかんともしがたいでしょう。

Re:

[Anonymous Coward]

要するに仕様に問題があることを証明できるわけですよね。
その延長として要求自体に問題があることも証明可能かもしれませんね。
そうなるとこんな会話が行われることになると。

「先日頂いたお客様の社内ルールを形式言語で記述して見たところ矛盾があるようです」
「我が社はずっとこのやり方でやってきて問題は無かった、そんな言い訳は許さない」
「では見逃している業務処理があるのだと思います、調べて頂けないでしょうか？」
「これまでもシステム化していないだけで、社内ルールを厳守してきた。問題ない」
「ですから矛盾がですね」
(以下略)

Re:

[Anonymous Coward]

そうすると「矛盾があることをないことにする」機能が言語に必要になって、
そういう部分をモジュールにまとめることで将来的なトラブル要素を一括して
管理できる矛盾管理モジュールが生まれることになります。

・・・これはこれで価値あるかも？