YOyogthos·Jul 2, 2018
Because static typing primarily focuses on showing that your types align. This is completely tangential to knowing that the code is doing what you intended.
In fact, it's often at odds with understanding the intent of the code because you're limited to a set of statements that can be verified by the type checker. This can make it harder for the human reader to understand what the code is meant to be doing.
For example, it takes nearly 300 lines of code to encode insertion sort using types in Idris https://github.com/davidfstr/idris-insertion-sort/blob/maste...
A human reader has to be able to read that and understand that the types are encoding the intent correctly. I don't know about you, but I have a much easier time knowing whether the dynamically typed version in Python is correct or not:
def insertionSort(lst):
for index
Read the rest
in range(1, len(lst)):
currentvalue = lst[index]
position = index
while position > 0 and lst[position - 1] > currentvalue:
lst[position] = lst[position - 1]
position = position - 1
lst[position] = currentvalue
Complex type definitions effectively become their own meta-programs that the compiler uses to verify your program, but now you've just pushed the problem back a step since somebody still has to read and understand the meta-program to know that it's verifying the correct thing.