> > the compiler verifies that either the user input string value will get turned into a `valid email` value at runtime or the user is asked to try again.
> 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.
There are two ways to have the compiler ensure that you produce safe SQL for any user input:
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, I am not saying that you cannot make any compile-time guarantees. I am saying that these have little to nothing to do with the actual securing against SQL injection attacks, and that the idea that static types help there is simply an unsupported assumption (and a circular argument, see parallel post).
> 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.