> When most practitioners think of "typechecking", they typically think about proving properties about programs statically.
This is what the type theory community (e.g. Bob Harper) thinks...not anyone else from what I can tell (definitely not practicing programmers).
Typing it out on mobile didn't make it easy to do the right quote context. Here is a good essay about it all:
http://www.cl.cam.ac.uk/~srk31/research/papers/kell14in-auth...
vs. say
https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
There are other ways to do typing that might make more sense for a dynamic language than going down the expressiveness rabbit hole; e.g.