河野真治 @ 琉球大学情報工学です。

In article <050218121108.M0154934@sma.gssm.otsuka.tsukuba.ac.jp>, kuno@gssm.otsuka.tsukuba.ac.jp writes
>   これもですね。論理学を学んで損ないのはもともと異論ないんです。
> 必須かと言われると違うでしょうという議論なんです。

僕は、
       日常言語と、論理学
ってのは、それほど差はないと思う。ちゃんと日常言語でコミュニケーション
できるってのは、論理学の基本を理解していることなんだよね。論理学の言葉
で言えば、
       命題論理の完全性
       述語論理の充足性
あたりを理解してないと日常会話できないと思う。これは、そんなに難しくない。

       「あったら○○牛乳買って来て」
       「なかったよ」
とか、
       「なんか、さっぱりしたもの食べたい」
       「そばは?」
とかですよね。

なんだけど、
       プログラム(や、仕様を含む仕事)に関するコミュニケーション
ってことになると、レベルがあがるんだと思います。おそらくは、
述語論理の非充足性とか証明可能性あたり。無矛盾性あるいは、型理論。

そういう意味で必須。特に、

        この入力の範囲に対して、このプログラムは正しく動く

っていうのを理解してない人がプログラムしたりすることは許されない
ことだと僕は思う。

なので、プログラム言語レベルで、それを要求
するってのは合理的だと思う。しかし、現状だと、
        enum hoge i;
        swich(i) {
で、enum が、すべて尽くされてないとかのWarning を出す程度なんだよね。

型理論は、広い意味で、

        ある範囲に対して、このプログラムは正しい

ってのをテストや検証よりもはるかに低いコスト、コンパイルのコストと
同じぐらいで示すことができるツールだと思います。

そのあたりに久野さんが異論があるとは思わないんだけど、そういうのを
要求しないプログラミングってのがありえるってことなのかな〜

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科

cf. Message-ID: <3991277news.pl@rananim.ie.u-ryukyu.ac.jp>
fj ニュースグループ管理委員(第11期)選挙中〜
  投票期間は 2/14(月) 〜 3/6(日) の3週間です。