Safe TypeScript: Safe and Efficient Gradual Typing for TypeScript
In this talk, we present Safe Typescript, a sound and efficient gradual type system for TypeScript. Our implementation of Safe Typescript is fully integrated into TypeScript (v0.9.5) as an optional “strict” mode which programmers can easily choose to enable or disable with a compiler flag.
We validate the usability and performance of Safe Typescript empirically by typechecking and compiling more than 118,000 lines of existing TypeScript code. We show that end-to-end overhead of runtime checks is small, particularly for code bases that already have type annotations. For instance, we bootstrapped the Safe Typescript compiler (90,000 lines, including the base TypeScript compiler), measuring only a 15% runtime overhead of type-safety while uncovering several programming errors as type-safety violations. We conclude that, at least during development and testing, Safe Typescript adds significant value at a modest cost.
Technical report: http://research.microsoft.com/apps/pubs/?id=224900
Online demo: http://research.microsoft.com/en-us/um/people/nswamy/Playground/TSSafe/
Aseem Rastogi is a PhD student at University of Maryland, College Park, advised by Mike Hicks. Here’s what he says about himself:
I am broadly interested in Programming Languages and Security. Most recently, I have been working on making Secure Multiparty Computations (SMCs) more practical by applying PL techniques. In particular, I have developed static analyses to optimize SMCs, and a new functional language, called Wysteria, to write reactive SMCs. At MSR, I am working with Nikhil Swamy on Safe TypeScript, a sound gradual type system for TypeScript.
- Aseem Rastogi
- University of Maryland