>カリーハワード同型対応や証明プログラミング
その昔流行した研究テーマですね

数学科で純粋数学に挫折して企業に就職した方が
上記のテーマで研究論文書いて学位を取得して大学に就職し
純粋数学の研究に戻っていきましたが…
http://www.ritsumei.ac.jp/se/~takayama/reHist.html

なかなか泣かせるヒストリーです