Liskov's work in this area focused on behavioral subtyping, which besides the type system safety discussed in this article also requires that subtypes preserve all invariants guaranteed by the supertypes in some contract. This definition of subtyping is generally undecidable, so it cannot be verified by a type checker.
Let the contract of operation
o of Type
T be that it halts for all inputs. Now decide whether operation
o of subtype
S <: T satisfies that contract: you have just solved the Halting Problem.
S::o must compute the same function as
S <: T. Deciding whether two programs compute the same function is called the Function Problem and is equivalent to solving the Halting Problem.
In general, statically deciding any non-trivial runtime property is almost always equivalent to the Halting Problem.
Because almost every question about the behavior of programs is undecidable. By Rice's theorem, any decision problem of the form:
Some programs compute functions that have this property, other programs compute functions that don't have this property. Given a program P, does the function computed by P have the aforementioned property or not?
is undecidable. So, for example, you can't always distinguish code that computes the square of an input from code that doesn't. Although in simple cases, it is often possible to prove that a function does or does not do so, there is no general procedure that works for all program.
Almost any interesting behavioral invariant falls under Rice's theorem, since those statements rarely (if ever) talk about what the method looks like internally, only what it returns and what side effects it causes in response to certain inputs.