I am not a teacher or researcher, I am a practicing programmer writing code that is used by critical systems as well as ambitious projects that will (hopefully) be used by many real people.
A red black tree is just an example with invariants that everyone is likely to know, so it's a nice way to illustrate the point about the power of types. Known problems are solved problems, and unsolved problems are unknown problems -- so either my invariants' example will not speak to you because you don't know it, or you will reject it because you can just re-use a library.