They're not at all opposite: one can think of reasoning about types as reasoning about UB. For instance, if a value is of type `int`, it's undefined behaviour f

They're not at all opposite: one can think of reasoning about types as reasoning about UB. For instance, if a value is of type `int`, it's undefined behaviour for it to be of type `float`, and so the compiler can optimise based on this fact (there's just the added bonus that the compiler also checks this UB "perfectly": code won't violate the rules). Essentially, undefined behaviour exposed to the user is an extra layer of "types"/rules on top of the underlying type system, both of which the compiler can use for optimisation purposes (but only one of which the compiler checks for the programmer). More and more advanced type systems can push more of the former into the latter (e.g. for index-out-of-bounds, in the limit, dependent typing can allow one to statically ensure that all integers are in range of the arrays they index).