[naasking]

> It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs

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.

[bykovich2]

"Practical" is the key word here, I believe.

[naasking]

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.