On: Why isn't mutable a subtype of immutable, or vice versa?

[antonvs]

> Types are properties of values, not variables.

In computer science, specifically programming language theory, types are properties of terms (syntactic expressions). It wouldn’t be possible in general to typecheck a program before running it if you had to have a value before you could discover its type.