>>181
20世紀の情報科学か、なにもかもみな懐かしい…

>その当時の学生にとっては、
>80年代は定理証明系と型を命題と捉えた
>カリー=ハワード同型対応プログラミング
>がせいぜいの所

90年代だったと思いますが、当時龍谷大にいた小林聡氏が
「実は古典論理でもカリー・ハワード対応で
　プログラム抽出できる」
という話をして
「えっ、今まで排中律を使うと構成的じゃないから
　プログラム抽出できないっていってたのは
　いったいなんだったんですか？」
と驚いたのをおぼえてますね

ま、今では常識なんでしょうけど
（詳しいことは
　照井一成氏「コンピュータは数学者になれるのか？」
　第５章　5.3　２つの論理　とか読んでください
　これ、いい本ですよ）