The holy grail of type theory is to write propositions as types and have proofs fall out of those propositions naturally. Those proofs comprise your program. So-called dynamic typing throws that all out the window and just says "I'll permit any program you want to write and bail out at the first opportunity". It's a proposition that is trivially true and thus it's not useful at all.