I can't give you a mathematical definition of it, but my intuitive one is that an unsound type system is a collection of kludges. It's relevant for programming because the language winds up with all kinds of ugly edge cases where things just don't line up right.

With a sound type system, you can do things like compose a new type out of other types, and it will work consistently (not produce weird edge behaviors).

For example, C's `void` type introduces anomalous behavior. A function returning `void` is not composable, e.g.:

    void foo();
    void v = foo();

would work in a sound type system, but does not work in C. You'll see it in the compiler implementation because it's a special case that appears over and over.