Just a nitpick: programming language theory makes absolutely no judgment on what is a correct or incorrect approach [1]. It just studies the implications of var

Just a nitpick: programming language theory makes absolutely no judgment on what is a correct or incorrect approach [1]. It just studies the implications of various language designs. In this case it says something close to, if you have erasure then you have parametricity, and it also says what parametricity guarantees. It does not and cannot, however, claim that this is the "correct" way. In general, mathematical theories do not have an intrinsic notion of empirical value. [1]: Although some PL theorists may, but this is an expression of their opinion, not something that comes out of the theory.