> someone said me that US air force is investing in type theory > so it is a place that you can have a job using theorem provers