[hyperpape]

At some level of abstraction, types of any kind are already proofs, and they're tremendously important in many actual existing languages.

What you're probably glomming on to is that efforts to push the bounds of what you can prove (higher kinded or dependent types) have had mixed results (mixed in the sense that some people think they're great, others are unconvinced).

So we're in a weird situation where many many people are using a tool, but relatively few are interested in new developments concerning how to use that tool.