A key word that had been disproven many times. The most recent example is Rust, which has a type checker that now type checks many previously unsafe C++ idioms. The other examples I listed are also quite practical, and have been used in high assurance systems.
Seems you don't know much about types then. I suggest you look up theorems provers and compcert and the TyPiCal language, as but a few examples.