Optimization and verification have already joined forces: just look at CrellVM [0], which made the rounds on HN some weeks ago. Also, as you mentioned, better t

Optimization and verification have already joined forces: just look at CrellVM [0], which made the rounds on HN some weeks ago. Also, as you mentioned, better type systems could be another nice byproduct. [0] http://sf.snu.ac.kr/crellvm/ http://sf.snu.ac.kr/crellvm/