Why would the term "dynamically typed" be considered a misnomer?
The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of &quot;type system&quot; given on the page before:

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

Note how aspects like &quot;syntactic method&quot; and &quot;classifying phrases&quot; mean that it applies to &quot;source&quot; programs, i.e., inherently is a static notion. Moreover, in actual type theory, programs that do not &quot;type-check&quot; are not even considered programs. The type system defines the set of well-formed programs. Something that's ill-typed has no meaning.
One could argue that this is the wrong definition. But it is shared by most researchers in the field and certainly by the ones working on type theory. It matches the notion of a &quot;type&quot; as established in mathematics and logic (lambda calculus, type theory). On the other hand, it would be difficult to come up with a sufficiently accurate definition of &quot;type system&quot; that would encompass &quot;dynamic typing&quot; without bordering on technically meaningless.
So from that technical point of view, a dynamic language is untyped, in the same way the untyped lambda calculus is (or equivalently, it has only one single type, such that every program is accepted as well-typed). Dynamic checks are not really on types but on the shape of values, which sometimes carry type-like &quot;tags&quot;.