A type system is an aspect of programming. I would hope a CS course covers type systems.

Proving something about a type system requires zero expertise in programming, debugging, git, Linux, C++, etc. And expertise in programming, debugging, etc., is of zero use in attempting to prove something about the type system.

As has been pointed out to me several times by CS academics, I could stand taking a course in type theory. I have a good intuitive sense about it (likely from my math background), but have no idea how to prove something about it.

A type system is an aspect of a logical system. You can have typed boolean algebras, I don't think anyone programs in those though.

A CS courseload certainly doesn't (and certainly not in the required selection of courses) cover soundness of a language. Even my theory-focused classload only covered automata up to proofs of regularity etc. This is, sort of, step 0 in soundness-proving methodologies, but it's only step zero.

The purpose of a type system is to ensure the correctness of programs. That's what they are, that's why they were invented, that's why they were studied. That CS involves math doesn't change the fact that its about programming.

You need to learn some history. Or at least cite your claims.

We use type systems to help abstract patterns of data into logical constructs that can be reasoned about. They are logic systems with grammar that describes relationships between axioms and constructs.

Seriously, go read a textbook and then we can pick this discussion up. Wikipedia has a good overview.

https://en.m.wikipedia.org/wiki/Type_theory

Ah, yes. Type theory originates before programming. Type theory only has relevance to computers insofar as it’s used to prove things about programs. Type theory in the context of computing is about programming.

We don’t call set theory and category theory “computer science” unless it’s about programming computers.

No, I mean that's an application yes, but I'd still call Alonzo Church a computer scientist and his work theoretical computer science.

Much as how people who study computability are computer scientist, even though none of the asymptomatic improvements to matrix multiplication since 1990 are even remotely relevant to any kind of real-life program.

That's one use, yes, but it isn't the only use. And it's certainly not why they were invented

Typed lambda calculus was formalized before the first programmable computers, and it's relation to programming wasn't clarified for another 20+ years (and real type systems don't really start to appear in programming languages for another decade after that afaik).

This is a narrow view on types; for example, types also help the compiler to produce optimized code. In general, they assist reasoning about and understanding the program.

What is an unsound type system. Why and how is it relevant for programing?

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.

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).

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.