This makes it much more likely to be used but it's fundamentally the same set of ideas.

A really cool idea I'm playing with at the moment is using fuzzing/static analysis based generators to feed spec/test.check.

I think it will help get past the, imo, biggest issue with generators in that they can miss exceptional cases in the code.

E.g. If (x=="jack and Jill) {exceptional case} is unlikely to be triggered with standard generators but "easy" for static analysis tools to solve.

> Also, with enough heavy lifting you can actually encode all of that in the types in a dependantly typed language like Idris [1]

In theory. In practice it is multiple orders of magnitude harder to prove properties in Idris than it is to spec them using property based testing.

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;
       }
    }