I don't think there is an underlying principle of compilers and language design that strictly prevents that. Implementing a static type checker seems like more

I don't think there is an underlying principle of compilers and language design that strictly prevents that. Implementing a static type checker seems like more work on the language designer, but from the end user (programmer)'s perspective, usually it comes down to preference and it doesn't seem that useful for the preference to be "both". If you're willing to specify types, then you get compile time checking benefits. If that's not worth the extra keystrokes, you might lean toward dynamic languages. Now, that said, there actually might be something close to what you're talking about. For one, many languages with static typing have very good type inference, so you don't always have to write the types in your code if the compiler can figure it out (infer it). Crystal is one of these languages (just off the top of my head). And among dynamically typed languages, some have static type checkers that can be used on top of the language, optionally. So that does give you a choice. For example, in Elixir and Erlang you can use Dialyzer to add static type analysis. Then still you have some languages that add static typing (and possibly other benefits) on top of a base language by transpiling. TypeScript/Javascript are a good example. What would be the benefit of creating a language where static type analysis was available, but not enforced? In my opinion, the benfit would be minimal, because static typing works best if it's enforced -- the point is to catch mistakes. If it's optional, how do you catch those mistakes?