Idle thought: you can view a type system as just an abstract interpretation of code. `x = 1` can be abstracted as assuming that x is a number, then checking that numbers are appropriate wherever x is used.