As someone curious about learning more about type systems, would you mind elaborating on 1.? I'm assuming you mean the formal definition of "sound", not just as a synonym for "sensible". Sound typing is often something handwaved away as not being particulary consequential in practice; what benefits have you seen there?