> Whether or not a particular email address is verified or not isn't something that's generally known at compile time Yes, obviously. What is knowable at compi

> Whether or not a particular email address is verified or not isn't something that's generally known at compile time Yes, obviously. What is knowable at compile time is the stuff that comes after: given that the input to this function has property X, does the output have property Y? Arguments, not premises. > But... (1) you can do the very same thing without types Sure, and if someone makes an SMT-solver-oriented language (that isn't just using it to drive type inference) I'll be happy to try it out. But what most people who dislike types claim is that you can replace them with testing (true in principle, false in practice: no one actually remembers to test every last edge case every single time) or just programmer discipline (lol).