[WalterBright]

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.

[Koshkin]

Isn’t that why some other languages explicitly draw a distinction between a function and a procedure? I think ‘void’ was introduced in C to do the same thing, implicitly (because omitting the return type does not achieve that).

[WalterBright]

Yes, but Wirth (Pascal's inventor) was an academic, which is why Pascal has a separate notion of functions and procedures. `void` is a hackish special case in the type system, and not just for function returns. It's unsound.