I don't claim that. Given what we know, the likeliest explanation to the findings so far is that an effect, if it exists, is probably small.
> Formal correctness? Bugs per line of code?
Both would work.
> in which case I think it’s basically a truism that more soundness leads to more correctness. At some cost, perhaps.
And you'd be wrong, or, at least, the second part of your statement makes all the difference. What we want is the best correctness we can get for some given cost, or, given some effort, what should you do to get the most correct program? If you follow formal methods, some of the hottest lines of research right now are about reducing soundness to improve correctness.
> As far as I could tell from reading the study, it’s not evidence that static languages encourage this sort of bug more.
I didn't say they did. But you asked how we explain the observation that types don't improve correctness, and one explanation is that the kind of mistakes that types catch aren't the costliest bugs that make it to production, and perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs.
> But this is the root of my reasoning.
That's as good a conjecture to start with as any, but it needs to be revised with findings.