1) as formally rich and fascinating as reality admits, and
2) ultimately grounded in guiding human experience
So far these have included shape/alias/region-analysis types for usable ownership, learned bayesian models of total point-to-point information flow in programs (for better error location), and now hardware design to enable performant code in the transactional memory model.