But OCaml and Rust infer types pretty well so people can avoid writing type annotations and still get quite far.

But yeah, it doesn’t nullify the argument that people have to be aware of the types of data they’re working with regardless.

Python, a dynamically typed language, has become very popular in introductory programming courses. If static types are helpful for programming, are they not also helpful for beginners? One hypothesis is that introducing a type system requires people to learn two notional machines (the type checker as well as the operational semantics) rather than just one, making learning the language harder. Is this right? How can we design type systems that we can show benefit beginners as well as experts? Or, alternatively, of the many different programmers doing different things, which might be better off starting with a strongly typed language?

Maybe a language where the type system is also defined in the language? Like Idris but more homoiconic?