Am I so crazy to want a general purpose programming language with

1. Reasonable abstraction facilities
2. Reasonable performance
3. Reasonably short, conceptual proofs of correctness for all relevant system properties (normalization, denotational semantics, etc.)

???

I think that this is in reach with the technology of SOGATs and Logical Relations as Types, and this is what I'm trying to do with Hippogriff.