Nice example with the nuclear missile. For those to whom this seems contrived, let me explain why the issue of type-safety and semantics is so important to me. I used to work in symbolic computation. In that world, it is very common for a large number of types to have the exact same operations, although they are semantically very different. Example: groups. If type-safety is a purely syntactical notion, then type is no longer a tool to enforce the distinction between different kinds of groups, such as abelian groups, torsion-free groups, etc.