Unsound typesystems are not necessarily a problem, but consider the problem the other way around: given a sound typesystem, how do we improve this in such a way

Unsound typesystems are not necessarily a problem, but consider the problem the other way around: given a sound typesystem, how do we improve this in such a way that a) the average Joe will understand it b) it decreases the overhead of writing the types c) the type system helps the programmer write better programs Haskells approach to this keeps the constraint of soundness: https://youtu.be/re96UgMk6GQ?t=52m5s https://youtu.be/re96UgMk6GQ?t=52m5s The whole video is very interesting even if you know nothing about Haskell, but are just interested in language design in general. To summarize the part of the video I just linked: Their approach so far has been to try and design the type system in such a way that you reduce programmer pain while not sacrificing soundness at all. It is a painful constraint for language designers, but it allows you to gradually add functionality to the type system from observing real world examples. The goal can be described as: Design a typesystem such that every working program can be typed in both a sound and correct way, while minimizing the amount of programs that can be typed, but are not working as intended.