今日も相変わらず数学のようなことをして過ごした.僕の専門は計算機科学にもよく応用されているけれど,本領は証明論における構成的な論理の下地作りであって,応用を前提とした構成になってはいない.コンピュータをある視点から捉えると,コンピュータの計算と僕が学生時代勉強したことのあいだに構造的な同型性が確認され,理論的な基礎付けに便利だから使われているだけだ.とするともう少し仕様上の綻びが目立ってもいいはずなのに,驚くほどそれがない.不思議だ.よくできた物語が,その著者も意図しなかった興味深い構造や関係,主張をしばしば表現するように,よくできた理論はその理論が本来表現しようとした範囲を超えて,真理みたいなものを多くの対象に与えることがある.