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.
