What you call "dynamic checking your types" is actually the same as having an algebraic uni type and inspecting its construction. A type system is a means to p

What you call "dynamic checking your types" is actually the same as having an algebraic uni type and inspecting its construction. A type system is a means to prove the absence of certain errors in a program. Think of a type system as a park pilot that sounds an alarm before you hit an obstacle. What python does is the crashing sound when you hit the obstacle. Forth is finding the dent days later and wondering where the eff that came from. Python is more conclusive then Forth, but you still have a dent.