Modern programming languages unlike older programming languages, or unlike assembly and machine code are typed. For example c++ with or without templates compared to c, or Java compared to Basic. 

With typing, a compiler needs to check that all expressions have the correct type. Generally, this is done by telling the compiler what types are being used. However, we can attempt to automate this process and allow the compiler to work out what the types are by itself, given the base types under consideration. This is known as type inference. 

Depending upon the language, type checking and inference can range from trivial to undecidable. 

We also say it is sound iff it accepts correctly typed programs.

Now, type checking and inference in the simply typed Lambda Calculus with parametric polymorphism is decidable and one implementation of this is the Hindley-Milner Type Sysyem where complexity is linear in the size of the program; however, the problem is PSPACE hard and EXPTIME complete, meaning that in the worst case scenario it requires a polynomial worth of extra space and an exponential amount of extra time. Luckily, it happens to be linear when the nesting depth of polymorphic variables is bounded.

For example, 

>1. C++ with templates is Turing complete by an informal proof by Veldhuizen '03. This means type checking and inference is undecidable. 

>2. In C#, both type checking and inference is undecidable. And it is unsound. 

>3. Similarly Java because Java Generics are Turing Complete. Amin and Tate '15 showed that Java 5 or later is unsound.

>4. Haskell has decidable type checking and inference. But with enough extensions, that is to at least System F, then it becomes undecidable as System F is.

Dependent types allow types to depend upon their values and so give a finer control over types. For example, with ordinary types you cannot have a type for even numbers; with dependent types you can. Unfortunately, adding this capability generally renders type inference undecidable.

Lean is a programming language which is based upon Calculus of Constructions with Inductive Tupes. This calculus is a higher order typed Lambda Calculus and lies at the top node of Barendregt's Lambda Cube. This means it has polymorphism and dependent types. 

It's main rival, is Martin Lof's Type Theory which is also dependent and inductive types. It comes in two main varieties, intensional and extensional. The intensional variety can be alternatively thought of as Homotopy Type Theory. In this variety, type inference is decidable whilst in the extensional variety it is not.

Set Theory like machine code, like assembly and like early programming languages are not typed. So type checking does not apply. As types allow us to program more safely, these languages are not as safe as typeful languages and hence, automation is more difficult here as we cannot prove they will act as we expect them to do so.