> No, the compiler cannot verify user input, because the compiler isn't running when the user is inputting data.
I'm not following why you thought I meant that. It's like you're arguing it's impossible to make any compile-time guarantees because you don't know what exact literal inputs your program will be dealing with at runtime when the field of https://en.wikipedia.org/wiki/Formal_verification exists. E.g. at compile time you can prove a sorting function gives the correct output for all possible inputs without having to run the code - you don't know in advance what the input is going to be (which is normal when coding), but you still know the output will be correct with respect to the function specification.
1. Define SQL in your type system, and force programmer to specify for any piece of user input they want to use in a query what its semantics are supposed to be. This is the SQL DSL approach, such as the short lived LINQ-to-SQL or Haskell's Selda. ORMs also do something similar.
2. Enforce that any string sent to the DB passes through some kind of checker that enures certain properties hold for that SQL. The checker will have to understand all of the semantics of SQL, just like in 1.
There are many libraries that go through path 1, but don't support the full capabilities of SQL (usually they support a tiny subset), even for a single DB.
No. Quite the opposite. People here confuse "static typing" with "checking stuff", even such obviously dynamic things as "checking outside input".
> You absolutely can at compile-time make sure your program is going to respond in a sensible way to problematic user inputs at runtime
Right. Sort of. But that is just normal code. Code that absolutely, definitely has to be executed at runtime and at no other time. Because that is when the actual users of your system are going to input the actual data. Not while you're compiling stuff. Your users (and the rest of the world you interact with) aren't there while you're compiling. And your compiler isn't around when your users are inputting data.
> the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime
No, the compiler cannot verify user input, because the compiler isn't running when the user is inputting data. You can implement a model that has the concept of "valid e-mail", and you can implement your system such that it converts input data such as strings into your structured model at the edges and then only deals with "valid e-mail" objects internally. But implementing such a model has nothing whatsoever to do with whether you use a statically type-checked language or a dynamically type-checked language.
It also turns out that such systems tend to be really, really bad. What you actually want to do is keep the user input exactly as it was input, for auditing purposes if nothing else, and build your structures as an enrichment on top of that basic data. Because your idea of what constitutes a "valid" e-mail is almost certainly wrong, and it's better if the system can at least represent data even if it doesn't completely understand it, rather than destroy user data.