You've said this same thing 3 or 4 other times in this thread.
Yes, yes, the formal definition of type inference as supported by languages like Haskell is not fully supported by C++, or Go, or C#, etc. But that's not the definition of it that anyone else in the comments here seem to be using, so can we drop it?
You seem to be knowledgeable about type theory. Is there a formalized term for the subset of type inference that C++11 supports? If so, can you just assume that others are using that term? Not that the discussion isn't interesting, but you're coming off as needlessly contrarian.
Whether a feature is a good or a bad thing to have is each programmer's subjective opinion. (But, of course, mine is diametrically opposed to yours: typeful programming would simply be impractical if you had to babysit the type-checker all the time.) OTOH, whether a language has or doesn't have a feature, is a technical fact.
It's not subjective at all. Features are good or bad for productivity. Maybe you have a different goal or have calculated the expected value differently, but with a well defined purpose it's not a subjective question.
> It's not subjective at all. Features are good or bad for productivity.
While productivity can be more or less objectively measured in the long run, the effects of a language feature on productivity vary from one programmer to another. There's no universal basis for evaluating this.
> Maybe you have a different goal
My primary goal is correctness. I don't really believe in 80% solutions. Having an incorrect program is just as good as having no program.
> have calculated the expected value differently
Very differently. My calculation is based on the following objective, unquestionable, technical facts:
(0) Determining whether the internal structure of a program is consistent (in the formal logic sense) involves lots of long, tedious and mostly unenlightening calculations.
(1) Computers are very good at performing long calculations. On the other hand, humans suck at it.
(2) Type structure, at least in sensibly designed languages, is the most efficient way known so far to communicate the intended logical structure of a program to a computer.
With type inference:
(0) The programmer only has to provide just enough information for the type checker to reconstruct the logical structure of the program.
(1) If the pieces fit together, the type checker will tell you exactly how.
(2) If the pieces don't fit together, the type checker will tell you exactly why.
OK, but you didn't specify a "well defined purpose". So what you said is obviously your opinion.
I find true type inference to be very helpful for readability. For example, you can write "let mut x = None;" where writing a type would be just noise.