Qual o significado da palavra Soundness no contexto de linguagens de programação?

Como eu não sou muito acadêmico responderei o que é mais necessário para entender, alguém mais ligado à teoria pode achar que não exatamente assim, vou falar só para entender porque a maioria das pessoas não precisam saber disso.

Qual seu significado dentro do contexto das linguagens de programação?

Isso tem a ver com robustez que eu sempre falo. Quando mais "sonoro" é o sistema de tipos de uma linguagem de programação, mais robusto o código tende ser porque essa sonoridade indica que o sistema de tipos não deixa produzir estados inválidos.

Fica claro que as linguagens de tipagem dinâmica tem baixa sonoridade. As de tipagem fraca podem ser piores ainda nesse ponto. Mesmo as de tipagem estática podem não ser tão sonoras assim, apesar de serem mais que as já citadas.

Linguagens de tipagem dinâmica que não possuem um mecanismo de generics não conseguem uma sonoridade tão grande. As que aceitam que o estado de um tipo seja inválido também baixa um pouco a sonoridade, por exemplo aceitando um valor null. Variância é outra sofisticação necessária para indicar todos estados possíveis.

As linguagens de mais alta sonoridade costumam possuir outros mecanismos como o higher kind type que dão garantias adicionais aos valores possíveis.

Essas garantias vão complicando a linguagem tanto para o uso quanto para criação do compilador. Então muitas linguagens preferem não ser tão soundness assim.

Haskell é uma linguagem de alta sonoridade, costuma-se dizer que depois de compilado um código em Haskell é certo que não tem erro, exceto se o problema foi mal definido.

Algumas pessoas consideram que deve verificar tudo em tempo de compilação para ser sonoro. Faz sentido, mas não sei se essa definição está estritamente certa, porque usamos o conceito matemático, que não tem compilação. Pode ser difícil provar que algo está errado em tempo de execução sem quebrar a robustez, mas eu não garanto que não é possível.

Até onde eu sei, se um sistema de tipos não deixa passar possíveis estados inválidos, mas também não deixa passar possíveis estado válidos, ou seja, ocorre o falso positivo, ele deixa de ser sonoro, porque ele foi pelo caminho fácil, não pelo caminho que provou a validade. Se você aceitar a premissa que falsos positivos não importam então qualquer linguagem que rejeite todos os códigos serão sound... e inúteis.

O que significa uma linguagem possuir um sistema de tipos Sound?

É justamente ter um sistema de tipos que pode expressar objetos da forma mais detalhada e que o estado seja sempre válido.

Não é que a linguagem tem um sistema de tipos sonoro, ela tem um nível de sonoridade. Eu só não sei dizer qual é o ponto que alguém usa para dizer que algo é sonoro ou não, e as pessoas fazem essas afirmações. Pelo menos no meu entendimento a linguagem consegue ser parcialmente sonora. Não sei porque em todas minhas pesquisas nunca achei algo dizendo sobre isso, então fico pensando se a pessoa diz "a linguagem X é sonora" ela sabe do que está falando. Se soubesse explicaria porque é. Se ela falar que um mecanismo específico da linguagem é sonoro aí é ok pra mim.

Sound é o jeito acadêmico de dizer que o sistema de tipos é seguro (não no sentido de invasão, mas de não deixar estados inválidos acontecerem e quebrarem o programa ou dar resultado errado).

Quais os benefícios?

A robustez é o principal deles, não deixa passar um código que não pode ser provado que está errado. Manter uma certa expressividade e documentação no código é outro, mas acho que está relacionado.

Há problemas em uma linguagem possuir um sistema de tipos desse tipo, se sim, quais?

A complexidade é um problema. Exige escrever muito código para atender tudo o que o compilador quer, costuma ser chato programar nessas linguagens. Algumas linguagens tentam fazer certas inferências, mas isso tem limite.