Ok, fair enough, but what about e.g. "-defer-type-errors" for GHC? I still think you're just arguing semantics. EDIT: Incidentally, the statically typed crowd

Ok, fair enough, but what about e.g. "-defer-type-errors" for GHC? I still think you're just arguing semantics. EDIT: Incidentally, the statically typed crowd can even go the "other way", namely from runtime -> compile time. For example, it's quite possible to derive a static proof/type from a runtime value in e.g. Idris by pattern matching as long as you're meticulous about building up the proof.