I am not sure about the motivation for this project but this article helps explain why some folks are interested in type systems as detachable (pluggable) components, separate from languages:
I've read a few of Gilad's papers - I just don't see how they can be practical in a world of third-party libraries (e.g. author A hates types, I like type-safety but I have to settle for none when I use that library).
This paper demonstrates an effective way of interfacing between typed and untyped code such that type errors can only happen at the boundaries - not within typed code.
I guess, but this seems like something that could become a best practice for library authors, and it'd be fairly trivial to retrofit or fork existing libs with annotations.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.175...