That would be an interesting tool.

Run a program while it is instrumented. The tool figures out what every type seems to be. Then goes back through the program and tries to prove that those types are correct.

It could then automatically annotate large chunks of code in a way that lets them run faster and will produce a warning if an unexpected type makes its way in in a future iteration. (An unexpected type, of course, being either a bug or a likely candidate for something that might expose latent bugs.)

I think you will be interested in this submission from a few months ago: Just-In-Time Static Type Checking for Dynamic Languages, https://news.ycombinator.com/item?id=11528375

That's basically how most JIT compilers work. But it would be nice to be able to get the annotations back out of the JIT. Anyone know of a JIT that lets you do that? (In any language, since now I'm just academically interested.) It that would be darned useful when one "inherits" a large, dynamically-typed code base... it would greatly increase freedom to refactor if you were more sure that such and such a function really does only ever get a number, despite all the code you see for handling objects and strings, for instance.

In Pharo (modern Smalltalk implementation) you can get some info from VM and JIT.

Someone is already working on type inference using VM caches.

See http://forum.world.st/parameters-of-the-virtual-machine-td48...

For python what does this do?

https://github.com/python/mypy/blob/master/mypy/stubgen.py

That's pretty close to what I'm currently playing around with.