This is called “the dead horse paper” for some reason. There’s been some interesting work since. This isn’t my exact area of research, but I’m pretty well versed in it and I work with one of the authors on this paper so I’m happy to try and answer any questions.
The chief issue here is how do you assign blame to typing violations? Typescript is unsound: since it just erases types, an untyped library that a typed component is using might return something the typed component isn’t expecting leading you to get a type error in typed code. Gradually typed python variants typically are better, though they usually just inspect the shape of the data and don’t check that eg every element in a list is correctly typed as well. This can lead to more unsound behavior. Typed Racket is fully sound, but performance can degrade spectacularly.
There’s been some work reviving the dead horse being beaten in this paper. Lmk if you have questions.
More papers:
Muehlboeck, Fabian, and Ross Tate. “Sound Gradual Typing Is Nominally Alive and Well.” Proceedings of the ACM on Programming Languages 1, no. OOPSLA (October 12, 2017): 56:1-56:30. https://doi.org/10.1145/3133880.
Moy, Cameron, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. “Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification.” Proceedings of the ACM on Programming Languages 5, no. POPL (January 4, 2021): 53:1-53:28. https://doi.org/10.1145/3434334.
Lazarek, Lukas, Ben Greenman, Matthias Felleisen, and Christos Dimoulas. “How to Evaluate Blame for Gradual Types.” Proceedings of the ACM on Programming Languages 5, no. ICFP (August 18, 2021): 68:1-68:29. https://doi.org/10.1145/3473573.
The chief issue here is how do you assign blame to typing violations? Typescript is unsound: since it just erases types, an untyped library that a typed component is using might return something the typed component isn’t expecting leading you to get a type error in typed code. Gradually typed python variants typically are better, though they usually just inspect the shape of the data and don’t check that eg every element in a list is correctly typed as well. This can lead to more unsound behavior. Typed Racket is fully sound, but performance can degrade spectacularly.
There’s been some work reviving the dead horse being beaten in this paper. Lmk if you have questions.
More papers:
Muehlboeck, Fabian, and Ross Tate. “Sound Gradual Typing Is Nominally Alive and Well.” Proceedings of the ACM on Programming Languages 1, no. OOPSLA (October 12, 2017): 56:1-56:30. https://doi.org/10.1145/3133880.
Moy, Cameron, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. “Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification.” Proceedings of the ACM on Programming Languages 5, no. POPL (January 4, 2021): 53:1-53:28. https://doi.org/10.1145/3434334.
Lazarek, Lukas, Ben Greenman, Matthias Felleisen, and Christos Dimoulas. “How to Evaluate Blame for Gradual Types.” Proceedings of the ACM on Programming Languages 5, no. ICFP (August 18, 2021): 68:1-68:29. https://doi.org/10.1145/3473573.