Como provar que seu código não tem erros de execução (e por que você provavelmente desistirá de tentar)
A interpretação abstrata permite provar que erros de execução são impossíveis antes da execução. Veja como ela funciona na prática, por que é difícil e onde se encaixa na sua cadeia de ferramentas.
Sua suíte de testes passa. Seu verificador de tipos está verde. Você faz o deploy. Duas horas depois, a produção lança um em um caso extremo que ninguém pensou…