런타임 에러가 없음을 증명하는 방법(그리고 왜 아마도 포기하게 될 것인지)
추상 해석은 실행 전에 런타임 에러가 불가능함을 증명하게 해줍니다. 실제로 어떻게 작동하는지, 왜 어려운지, 그리고 도구 체인의 어디에 맞는지 알아봅니다.
테스트 스위트는 통과했다. 타입 체커는 초록불이다. 배포했다. 두 시간 후, 프로덕션에서 아묏도 테스트하지 않은 엣지 케이스에서 가 발생했다. 테스트는 버그를 찾는다. 타입은 일부를 방지한다. 둘 다 프로그램이 런타임 에러로부터 자유롭다는 것을 증명하지는 못한다. 그것을 위해서는 더…