[thesz]

I once read lispers discussion on Qi language. One (actual) Qi user told us that he managed to prove that number 42 has type String.

This is the price of optional typings. It leave random holes in your program.

[jamii]

This paper presents an optional type system where type errors can only occur in the untyped sections:

http://homepages.inf.ed.ac.uk/wadler/papers/blame/blame-sche...