Existe uma diferença entre segurança e solidez do tipo?

Eu tenho tentado separar as definições de segurança de tipo e solidez de tipo e estou me divertindo muito. Perguntei recentemente a um professor e, depois de pensar um pouco, ele disse que realmente não havia diferença. No entanto, depois de ler isso , parece que:

• O Type Safety é uma propriedade da linguagem que diz que a aplicação de funções (e operadores) aos dados é significativa (ou seja, 1 / "Hello" não faz sentido e não é permitido)
• A solidez do tipo é uma propriedade de um sistema de verificação de tipo que garante que suas previsões de tipo estático sejam precisas em tempo de execução.

Isso é claramente apenas uma anotação de uma pessoa e estou me perguntando se existe algum padrão na comunidade de PL. Eu fiz algumas pesquisas e não encontrei uma resposta satisfatória.

Segurança de tipo e solidez de tipo são sinônimos na maioria dos trabalhos teóricos. A solidez do tipo é frequentemente formulada com relação a uma semântica operacional como preservação e progresso (do tipo). A preservação afirma que, se uma expressão tiver algum tipo, depois de uma etapa de avaliação (por meio da semântica operacional), a expressão resultante poderá receber o mesmo tipo. O progresso afirma que, se uma expressão não for um valor, ou seja, não for totalmente avaliada e for bem digitada, poderá ser avaliada posteriormente.

"Segurança de tipo" e "solidez", mas particularmente "segurança de tipo", também são amplamente usadas pela comunidade de programação (não-teórica), geralmente de maneiras vagas, ambíguas ou totalmente incorretas. Por exemplo, uma API que usa tipos de enumeração em vez de permitir seqüências arbitrárias quando apenas um subconjunto é significativo, digamos, pode ser chamada de "mais seguro para o tipo", mas essa declaração não faz sentido usando a definição teórica de "tipo seguro ", que é uma propriedade binária do idioma como um todo.