2007-09-15プログラムは計算機を前提に書かれるのだから、計算機の構造と動作を理解していることは重要であることは間違いない。プログラムは仕様を満すために書かれるのだから、仕様の形式的記述と検証について理解していることは重要(かもしれない)。 (用語、概念をいいかげんに使っているので絶対に真にうけないこと!!) (マシン語を知らない子ども達 - UEI shi3zの日記とこれに対する反響を読んで書いたものです) あまりにも当たり前過ぎて21世紀に入ってから言葉にしたことはあまりないのですが，当然のことながら，プログラムというのは，Curry-Howardの対応を理解して、初めて「書ける」と言うものです．プログラムが書ける，という状態は「Curry-Howardの対応を理解している」という状態の延長線上にあるべきで，Curry-Howardの対応を理解していないということは，プログラムの仕様を理解していない
