Wie man beweist, dass Code keine Laufzeitfehler enthält (und warum man wahrscheinlich aufgibt, es zu versuchen)
Abstrakte Interpretation ermöglicht es, Laufzeitfehler vor der Ausführung als unmöglich zu beweisen. So funktioniert es wirklich, warum es schwierig ist und wo es in die Toolchain passt.
Die Testsuite ist grün. Der Typchecker ist grün. Man deployt. Zwei Stunden später wirft die Produktion einen bei einem Edge-Case, an den niemand gedacht hat.…