Sound and unsound aren’t the same as strong and weak. Weak and strong systems aren’t honestly very well defined, but under many definitions can be both sound and unsound, though the theory of the weak system will need to have explicit inclusion of the implicit casts (e.g.).
Type systems become unsound when they, as a total system, cannot uphold their own promises. The promises of a weak system are weaker, but not (always) non-existent. In an unsound system you can generally, through trickery, take any expression reducing to a value of some type and modify it so that it appears to reduce to any other type at whim.
> Weak and strong systems aren’t honestly very well defined
I see, but at least the literature I read on typing actually mentioned them. Nothing I read in college regarding type systems ever included the words "sound" or "unsound".
> some type and modify it so that it appears to reduce to any other type at whim.
I saw instances of this as examples of "weak" typing.
Do you happen to have papers or books you could recommend so that I can learn more on type system soundness? This is a subject that I find really interesting.
How were weak and strong defined in the literature you read?
Anyway, more on soundness. I can recommend a couple papers:
Wadler (inventor of the monad) wrote a paper called "Well-Typed Programs Can’t Be Blamed" [0] about soundness.
There was a recent paper that made the rounds about how java's type-system is provably unsound as well that's worth reading [1].
I second the parent comment that weak and strong are ill-defined in my experience, while sound/unsound have well-accepted definitions and are commonly used in academia. Your experience obviously differs for whatever reason.
You can find many other references to soundness in the citations of those papers, as well as scattered around the internet.
Type systems become unsound when they, as a total system, cannot uphold their own promises. The promises of a weak system are weaker, but not (always) non-existent. In an unsound system you can generally, through trickery, take any expression reducing to a value of some type and modify it so that it appears to reduce to any other type at whim.