Being "sound" just means you can prove things are consistent with the assumptions you can encode in it. If there are things you can't encode in the types, or if your assumptions are wrong (misapprehension being one of the main problems in software), or if your requirements change, soundness is not going to save you.
Static types and proofs are valuable. Programs like compilers have fixed inputs and outputs and are excellent places to lean on things you can prove. But most of the programs I've worked on are not like compilers. They run for years, the requirements change, they have to deal with dirty data, talk to other messy systems, etc. And I'm not saying that dynamic types are perfect either.
My point is simply that static types are not a magical end goal of programming. They are a tool with tradeoffs.