On contrary, empirical studies done in the 90's and such by the likes of Mitre Inc showed people using Ada and C++ were more productive than C developers while producing way less defects. That the language and libraries were designed specifically to counter hard-to-track issues were one of the reasons why. That languages would improve safety was known far back as MULTICS with PL/0 where it's prefixed strings and reverse stack prevented two of the most common crashes/hacks in UNIX/C land.

The evidence is on our side that well-design language significantly reduces number of defects in production code if other variables are equal.

Where's this "proof" you speak of?

By contrast, strong static typing does in fact prove the absence of certain errors.

Where are all the use-after-free bugs leading to remote code execution (for example) in projects written in languages other than C or C++?

That is blatantly false. Type-safety can prove (as in a mathematical proof) that whole classes of bugs are impossible.