カリーハワード同型対応を使って型プログラミングをすると、
問題領域に応じた適切な命題を作る能力と、
命題を漏れなく証明をする能力が磨かれる。