Why would the term "dynamically typed" be considered a misnomer? In the book &quot;Types and Programming Languages&quot;, the author writes:

The word &quot;static&quot; is sometimes added explicitly - we speak of a &quot;statically typed programming language&quot;, for example - to distinguish the sorts of compile-time analyses we are considering here from the dynamic or latent typing found in languages such as Scheme, where run-time type tags are used to distinguish different kinds of structures in the heap. Terms like &quot;dynamically typed&quot; are arguably misnomers and should probably be replaced by &quot;dynamically checked&quot;, but the usage is standard.

I am not sure if I understand this. Does the author mean that, in type theory, all programs are &quot;statically typed&quot;?
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;.