Leanで健全性を証明した検証器が、TypeScriptの型安全性を「証明付き」で保証する
TScert: A Sound Core for TypeScript
TypeScriptの型チェッカーはanyや型アサーション、未チェックの配列アクセスによって意図的に不健全な箇所を残している。TScertは独立した検証器で、Leanで健全性が証明されたチェッカーが証明書を検証し、合格した関数だけを受け入れる。TypeScriptやツールが推論した型は一切信用しない。研究プロジェクトであり、v0.94時点でtools/内の686関数のうち643関数を検証済みだ。
TypeScriptの型チェッカーは意図的に不健全な箇所がある。any、型アサーション、未チェックのインデックス読み取り、共変配列によって、tscを通ったプログラムが型ではstringとされている箇所でundefinedを読めてしまう。