> That's not super interesting (to me personally, an acknowledged idiot) because working programmers are hardly ever confused about types. Intellij pretty much already does that thing.

One reason it's nice to have "toy models" and proofs is that we can gain confidence about how our "foundations" will/won't behave.

For example, Java's type system is well understood; it has some problems (e.g. https://dev.to/rosstate/java-is-unsound-the-industry-perspec... ), but we can think of them happening in 'contrived edge-cases', and we can make conservative claims about what is/isn't a 'contrived edge-case' (i.e. "that looks reasonable" vs "don't do that, even if it works").

Since we have a good understanding of Java's type system, we can do things like generating Java code automatically; this may be as simple as getters/setters in an IDE, or as complicated as a full API compatibility layer (e.g. swig, and many others). Automatically generated code can be very strange, but it's fine if we know that only "reasonable" code will be generated.

Let's compare this situation to IntelliJ's inference features. To make a more apples-to-apples comparison, let's turn IntelliJ's features into programming language features: we make a new language, which looks like Java but doesn't need as many type annotations. Our compiler takes the code it's given, fires up IntelliJ on a headless remote desktop, pastes in the code, clicks on some "infer types" button, copies out the result, kills the IntelliJ/desktop and feeds the generated code to javac.

The question is: what are the rules of our new language? Do we know what code looks "reasonable" and what looks like an "edge-case"? What properties can we be confident about? For example, can we make a claim like "return type annotations aren't required when calling a method"? How can we be sure? If our language does have such properties, do they work nicely together? For example, if we can do `a = b.c();` without annotating `a`, and we can do `a.b(c);` without annotating `c`, can we compose these together to do `a = b.c(d.e())` without annotating `a` `e`? Imagine how frustrating it would be if we couldn't be confident about what would/wouldn't work; all we could do is hit "compile" and cross our fingers, and if we did encounter a problem we wouldn't be sure about how to work around it. Third-party libraries which work perfectly well on their own might cause errors when used together; should we ask upstream to fix their (working) code? Should we abandon the libraries, or maintain in-house patches?

Now imagine that we're writing a code generator; e.g. a port of swig to our new language. What sort of code should we emit? How can we be sure that it'll work, regardless of whatever curveballs our users throw at us?

Even if we surmount all of these challenges, with a mountain of regression tests, what happens when IntelliJ push an update and a bunch of those tests break; do we start by rewriting our language's documentation?

This is why it's useful to have a small, self-contained system (like MLsub) which we can reason about semi-easily; which we can prove properties about. Even if we have to restrict things, like only proving something for a subset such that XYZ, at least we know what those limitations are.

Real systems can then be built on this foundation, with confidence about what can and can't be done.