Curry-Howardの対応を知らない子ども達

(用語、概念をいいかげんに使っているので絶対に真にうけないこと!!)
(マシン語を知らない子ども達 - UEI shi3zの日記とこれに対する反響を読んで書いたものです)

あまりにも当たり前過ぎて21世紀に入ってから言葉にしたことはあまりないのですが，当然のことながら，プログラムというのは，Curry-Howardの対応を理解して、初めて「書ける」と言うものです．プログラムが書ける，という状態は「Curry-Howardの対応を理解している」という状態の延長線上にあるべきで，Curry-Howardの対応を理解していないということは，プログラムの仕様を理解していない，つまりプログラムを理解していないのとほぼ同じことだと思います．

最近はLLと呼ばれる，いわゆる軽量スクリプト言語がメインになってきていますし，僕も普段はPHPでプログラムを書くことが増えてきましたが，それでも依然として，プログラムというのはCurry-Howardの対応を理解して書くもので，プログラムというものはすべて型付λ算法の延長上にあると思っています．

その意識がないと、たとえPHPやJavaScriptのコードを書いていても、不可解な動きをしたり、遅くなってしまったりしたときに「なぜだろう?」ということがピンとこないことになります。

まだ大学に入って無くて、趣味のプログラミングを楽しんでいる若い人たちには、ぜひCurry-Howard対応にもとづくプログラミングを勉強してみることを勧めます。

最近は素晴らしい時代になったもので、ごく初歩的な入門はHaskell言語などの静的型システムをもつ言語でもすることができます．

しかし本格的にCurry-Howard対応で遊びたくなったら、AgdaやCoqなどの定理証明支援系を使うのがお勧めです．

今のプログラム仕様は複雑になりすぎていて、初心者が全ての性質を知ろうとすると膨大な時間と労力がかかります。

しかし、最終的にはそれは全て知らなければならないことですし、知っておくべきことです。

最近は、全くの文化系の女の子が、わずか数ヶ月の研修で「システムエンジニア」や「ITコンサルタント」と称してJavaのプログラムを書くような商売もあるらしいのですが、そんなときにもぜひCurry-Howardの対応を勉強してもらいたいと思います。Curry-Howardの対応が解らないと、そもそもシステムが満すべき仕様の構造やその証明の構成方法がわからないということなので、何が問題なのかわからないことの方が多くなると思います。

どれだけデバッガやコンパイラが進化しても、その仕組みを理解していることは絶対に必要です。

筆算ができない人が電卓を使い続けたときに答えが正しいのか間違っているのかわからないのと同様，Curry-Howardの対応が理解できない人が書いたプログラムは、一見うまく動いているように見えたとしても、それは奇跡のようなバランス、自転車で言えば補助輪がついた状態で奇跡的に動いているに過ぎず、なにか未知の問題が発生したときに素早くプログラムの仕様内部でおきていることに直感を巡らせ、適切な処置・対応をするためにはCurry-Howardの理解は不可欠と言って良いでしょう。

さらにいえば、Curry-Howardの対応よりさらに下のレイヤーである、直観主義論理学を理解しているとさらに理想的です。

昔、形式的仕様記述の本といえば論理学の本を意味しました。しかし、今の若いプログラマ達は、下のような証明図をみても何を意味するか瞬時にわからないのではないでしょうか．(図は略)

プログラムは全て論理式とその証明の組み合わせでできています。プログラムを構成するのは全て直観主義論理なので、直観主義論理を理解しないとシステムの満すべき性質を理解していないことになります。

最低でも、一階述語論理系を構成できる程度の理解はしておいて欲しいと思います。

直観主義論理，Matin-Loefの型理論、依存型算譜言語の3つは、現在でもあらゆるプログラムの基礎になっているので、最低限おさえておきたいところです。

最後に参考文献をまとめておきます。

ただ読むだけでもとても面白い記事ばかりです。

http://itpro.nikkeibp.co.jp/article/COLUMN/20070909/281498/?P=1&ST=develop
http://d.hatena.ne.jp/yoshihiro503/