Note that weak typing and dynamic typing are orthogonal. I believe you're expressing sympathy for strong dynamic typing: types are checked an enforced dynamica

Note that weak typing and dynamic typing are orthogonal. I believe you're expressing sympathy for strong dynamic typing: types are checked an enforced dynamically by the runtime (such as Python raising an exception if you try to add a string and an int), but there's no static type analysis done at compile / load time. Python, JS, Ruby, etc. are strong dynamically typed languages. Also, type weakness is more a property of the runtime than the language, but for those languages with specifications, the language specification usually also specifies a large amount of behavior for a compliant runtime. The C runtime, will gladly (with UB nasal demon caveats) allow you to treat an int as a pointer. There are static type checks, but no hard limits on the type-confused nonsense it will attempt to execute. C is statically typed, but weakly typed. Java, C#, etc. are strong statically typed. There are static checks at compile time, and the runtimes do their best (modulo escape hatches) to use dynamic runtime type checks to plug the gaps in the static type systems. (For any sufficiently complex sound/consistent type system in a Turing-complete language, as per Godel's incompleteness theorem and the halting problem, there will be some programs that cannot statically type-check but still will never encounter a type error, regardless of input. So, in practice, there will always be escape hatches in the type system to allow programs that are correct but not provable. Hopefully most of these escape hatches are backed by dynamic runtime checks.) Of course, these categories are a partially-ordered continuum, not clear binary distinctions. For some pairs of languages, you can say one's statically enforced properties are a superset of the other or that one runtime enforces a strict superset of the other's dynamic checks. However, it's often a case that you can't say one language strictly offers stronger static type guarantees or one runtime strictly enforces stronger dynamic type restrictions.