１２９です。

「命題＝型、証明＝プログラム」な「構成的ブログラミング」
って、今どーなっているのか、誰か教えて！

(型推論と逆の話になると思う... )