You don't even need a type system to eliminate memory unsafety. Show me the memory unsafety in lambda calculus. (and don't forget that, as you said, we're talking about languages, not runtimes)