Cómo demostrar que tu código no tiene errores en tiempo de ejecución (y por qué probablemente desistirás)
La interpretación abstracta te permite probar que ciertos errores en tiempo de ejecución son imposibles antes de ejecutar el código. Así es como funciona en realidad, por qué es difícil y dónde encaja en tu cadena de herramientas.
Tu batería de pruebas pasa. Tu verificador de tipos está en verde. Haces el despliegue. Dos horas después, producción lanza un en un caso extremo que nadie…