[oivey]

Suppose you write a program that computes the sum of two input numbers. Suppose the two inputs are 1 and “a”. If it returns “1a” or 12 or whatever, the program is incorrect. Its correctness does not hinge on type safety. A untyped program could detect that one of the inputs is unexpected and correctly raise an error. Typing may make it easier to detect this error (or not). Fundamentally, adding type information does not make the above program “more” correct. It’s either correct, or it’s not.

You can write a sorting algorithm in assembly, and it can be correct. Rewriting in Haskell won’t make it “more” correct.

There’s an undercurrent of people espousing strictly types languages (not accusing you) who believe that somehow programs written in them are better. They’re not. They either serve their purpose, or they don’t. Strict typing is a tool. Sometimes it’s enabling. Sometimes (example: horrible polymorphism in most strictly typed languages like C++/Java/copy cats) it’s a hinderance. Strictly typed languages aren’t strictly better than non-strictly typed ones.