Is correctness or verification a question of test vs. type (because dynamic languages as Python or Ruby without strong typing can not be relied on to create large programs) ? It is true that testing is especially important for dynamic languages, and sometimes neglected for traditional, strongly typed languages as C# or Java. I think both testing and type checking can be considered as self-verifying and self-inspecting code.
Quinn Dunkan says about test vs. type (see here and here):
“The static people talk about rigorously enforced interfaces, correctness proofs, contracts, etc. The dynamic people talk about rigorously enforced testing and say that types only catch a small portion of possible errors. The static people retort that they don’t trust tests to cover everything or not have bugs and why write tests for stuff the compiler should test for you, so you shouldn’t rely on only tests, and besides static types don’t catch a small portion, but a large portion of errors. The dynamic people say no program or test is perfect and static typing is not worth the cost in language complexity and design difficulty for the gain in eliminating a few tests that would have been easy to write anyway, since static types catch a small portion of errors, not a large portion. The static people say static types don’t add that much language complexity, and it’s not design “difficulty” but an essential part of the process, and they catch a large portion, not a small portion. The dynamic people say they add enormous complexity, and they catch a small portion, and point out that the static people have bad breath. The static people assert that the dynamic people must be too stupid to cope with a real language and rigorous requirements, and are ugly besides.”
4 Lines of Code 