¿Hay alguna diferencia entre seguridad de tipo y solidez de tipo?

He estado tratando de separar las definiciones de seguridad de tipo y solidez de tipo y me lo estoy pasando muy bien. Le pregunté a un profesor recientemente y después de pensar un poco me dijo que realmente no había ninguna diferencia. Sin embargo, después de leer esto , parece que:

• Type Safety es una propiedad del lenguaje que dice que la aplicación de funciones (y operadores) a los datos es significativa (es decir, 1 / "Hola" no tiene sentido y no está permitido)
• Type Soundness es una propiedad de un sistema de verificación de tipo que garantiza que sus predicciones de tipo estático sean precisas en tiempo de ejecución.

Esto es claramente solo una nota de personas individuales y me pregunto si hay algún estándar dentro de la comunidad PL. He buscado un poco y no he encontrado una respuesta satisfactoria.

La seguridad del tipo y la solidez del tipo son sinónimos en la mayoría de los trabajos teóricos. La solidez de los tipos a menudo se formula con respecto a una semántica operativa como (tipo) preservación y progreso. La preservación indica que si una expresión tiene algún tipo, luego de un paso de evaluación (a través de la semántica operativa), la expresión resultante puede recibir el mismo tipo. El progreso indica que si una expresión no es un valor, es decir, no se evalúa completamente y está bien tipada, entonces se puede evaluar más a fondo.

La "seguridad de tipo" y la "solidez", pero particularmente la "seguridad de tipo", también son ampliamente utilizadas por la comunidad de programación (no teórica) a menudo de manera vaga, ambigua o totalmente incorrecta. Por ejemplo, una API que usa tipos de enumeración en lugar de permitir cadenas arbitrarias cuando solo un subconjunto es significativo, por ejemplo, podría denominarse como "más seguro para los tipos", pero esta declaración no tiene sentido utilizando la definición teórica de "tipo seguro ", que es una propiedad binaria del lenguaje en su conjunto.