TypeScript 코드를 Lean 증명으로 검증하는 TScert, tsc가 통과시킨 함수를 거부하다
TScert: A Sound Core for TypeScript
TypeScript의 타입 검사기는 any, 타입 단언, 미검사 인덱스 접근, 공변 배열 때문에 의도적으로 불건전한 부분이 있다. TScert는 TypeScript 컴파일러 API로 소스를 읽고, OCaml 프로듀서가 제안한 타입 주장을 신뢰하지 않은 채 Lean으로 옮긴 뒤 증명 인증서를 검사해 함수를 받아들인다. Lean에서 건전성이 증명된 검사기가 인증서를 검증하며, any와 타입 단언은 거부한다. 연구 프로젝트로 v0.94에서 tools/의 686개 함수 중 643개를 검증했다.
TypeScript의 타입 검사기는 의도적으로 불건전한 곳이 있다. any, 타입 단언, 미검사 인덱스 읽기, 공변 배열 때문에 tsc를 통과한 프로그램이 타입이 string이라 말하는 자리에서 여전히 undefined를 읽을 수 있다.