> software inherently has bugs for as long as we use type-unsafe languages This is untrue. Textbooks on type theory (Pierce’s TaPL comes immediately to mind) w

> software inherently has bugs for as long as we use type-unsafe languages This is untrue. Textbooks on type theory (Pierce’s TaPL comes immediately to mind) will state early on that well typed terms cannot always eliminate all undesirable states. In fact, there is a tension in encoding all your constraints into the type system (at which point you become a mathematician proving theorems) and producing programs that are actually useful to other people.