2 ms·
To add to what sheepmullet said, I think the insertion sort example is exactly the problem with advanced type systems. It takes nearly 300 lines of code to prov
by yogthos 9y ago
To add to what sheepmullet said, I think the insertion sort example is exactly the problem with advanced type systems. It takes nearly 300 lines of code to provide the specification.
Somebody has to be able to read that specification and understand that it's correct in a semantic sense. Ultimately, the specification itself becomes a full blown program that the type checker executes. So, now you run a program to try and verify aspects of your original program, but how do you verify that the specification itself is correct?
At some point a human has to be able to read the code and decide that it matches the intent. This step can't be automated, and I certainly don't think the Idris example improves things. I'd argue that it's far easier to tell that this version is correct:
fun insertionSort(arr, int n)
{
var i, key, j;
for (i = 1; i < n; i++)
{
key = arr[i];
j = i-1;
while (j >= 0 && arr[j] > key)
{
arr[j+1] = arr[j];
j = j-1;
}
arr[j+1] = key;
}
}