What's wrong with subtypes and inheritance?

While working on the formal verification of some software, I was introduced to Shapiro's work and went down a rabbit hole learning about BitC, which I now understand is foundational for the existence of today's Rust. Even though Shapiro made sure to scrub as much as possible any information on the internet about BitC, some writings are still available, like this retrospective.

Shapiro seems to be very much against the concept of subtyping and inheritance with the only exception of lifetime subtypes. Truth to be told today's rust neither has subtyping nor inheritance, except for lifetimes, preferring a constructive approach instead.

I'm aware that in the univalent type theory in mathematics the relationship of subtyping across kindred types leads to paradoxes and hence is rejected, but I thought this was more relevant to axiomatic formulations of mathematics and not real computer science.

So why is subtyping/inheritance bad in Shapiro's eyes? Does it make automatic formal verification impossible, like in homotopy type theory? Can anyone tell me more about this?

Any sources are more than welcome.

EDIT: For future reference, this provides a satisfactory overview of the problem.