Y a-t-il une différence entre la sécurité du type et la solidité du type?

J'ai essayé de démêler les définitions de la sécurité des types et de la solidité des types et j'en ai un sacré moment. J'ai demandé à un professeur récemment et après un peu de réflexion, il a dit qu'il n'y avait vraiment aucune différence. Cependant, après avoir lu cela, il semble que:

• La sécurité de type est une propriété du langage qui dit que l'application de fonctions (et d'opérateurs) aux données est significative (c.-à-d. 1 / "Bonjour" est un non-sens et n'est pas autorisé)
• La solidité du type est une propriété d'un système de vérification de type qui garantit que ses prédictions de type statique sont précises au moment de l'exécution.

Il s'agit clairement d'une simple note individuelle et je me demande s'il existe une norme au sein de la communauté PL. J'ai fait quelques recherches et je n'ai pas trouvé de réponse satisfaisante.

La sécurité des types et la solidité des types sont synonymes dans la plupart des travaux théoriques. La solidité du type est souvent formulée par rapport à une sémantique opérationnelle comme (type) conservation et progression. La préservation stipule que si une expression a un certain type, puis après une étape d'évaluation (via la sémantique opérationnelle), l'expression résultante peut recevoir le même type. Progress indique que si une expression n'est pas une valeur, c'est-à-dire qu'elle n'est pas entièrement évaluée et qu'elle est bien typée, alors elle peut être évaluée davantage.

La "sécurité de type" et la "solidité", mais en particulier la "sécurité de type", sont également largement utilisées par la communauté de programmation (non théorique), souvent de manière vague, ambiguë ou carrément incorrecte. Par exemple, une API qui utilise des types d'énumération au lieu d'autoriser des chaînes arbitraires lorsque seul un sous-ensemble est significatif, par exemple, pourrait être qualifiée de "plus sûre pour les types", mais cette déclaration n'a pas de sens en utilisant la définition théorique de "type sûr "qui est une propriété binaire de la langue dans son ensemble.