> Take the spec for all sorting algorithms (giving observational equivalence):
It's not that simple. You also have to specify the effect set of the algorithm, meaning, assuming we do in place sort: every memory cell other that the input array are unchanged after termination. (If you return a fresh array, you have to specify something related). You also have to specify what happens for general sorting predicates, for example if the sorting predicate prints out the element it compares then this reveals (much of) the algorithm.
> The compression is stripping away the 'how'
The sorting example shows that this largely doesn't work in practise. In my experience for non-trivial programs you tend to have to carry around invariants whose complexity matches the size of the program you are verifying.
> I'm convinced that larger scale proof automation is way more essential than HoTT.
I strongly agree, but currently this proof automation is largely a hope, rather than a reality.
> crazy type hackery as seen in Haskell or Scala
Haskell and Scala have (local) type-inference. That makes those complex types (somewhat) digestible.
> dependent types just for refinement
If / when this really works well, so that you don't pay a price when you are not using complex types, then this would be very nice. I don't think PL technology is there yet. (I'm currently using a refinement typing approach in production code.)
>It's not that simple. You also have to specify the effect set of the algorithm, meaning, assuming we do in place sort
I implicitly assumed that state would be encapsulated, since after all dependent types are fundamentally incompatible with observable state, but you're right that this is part of the spec. However I have severe doubts about the usability of any specification language that takes more than a one-liner to specify this.
>You also have to specify what happens for general sorting predicates
If you want to admit more general sorting predicates, sure, but normally you'd just allow pure functions.
>The sorting example shows that this largely doesn't work in practise. In my experience for non-trivial programs you tend to have to carry around invariants whose complexity matches the size of the program you are verifying.
If you include lemmas derived from the spec then I'd agree, but then the spec you have to check would still be a lot smaller. If not, then the only specs where I've experienced anything close to this are ones that are just the operational semantics of existing programs i.e. cases where you want to analyze a specific program. Otherwise I'm frankly uncertain as to what even the point of giving a spec would be.
>Haskell and Scala have (local) type-inference. That makes those complex types (somewhat) digestible.
Might make it more tractable to use, but I find my issue is that it's less direct and often obfuscates the meaning.
> doubts about the usability of any specification language that ...
You can extrude hidden state in ML-like languages, which gives rise to all manner of subtle behaviour in combination with higher-order functions. As Pitts, Odersky, Stark and others have shown in the early 1990s, even just the ability to generate fresh names (in ML-like languages, this corresponds to the type Ref(Unit)), in conjunction with higher-order functions gives you essentially all the specification and reasoning problems of state.
> normally you'd just allow pure functions.
This is way too restrictive for non-trivial programs. This restriction work for sorting. And in reality even there you'd run into problem, for example if you take into account that a predicate might throw an exception (which, in practise you cannot avoid, think overflow or taking the head of an empty list).
> the only specs where I've experienced anything close to ...
I think that's because you have not attempted to prove substantial theorems about substantial code. The SeL4 verification is interesting in this context: it's specification (a purely functional specification of the OS behaviour) had, IIRC about 1/3 of the size of the OS's C code. Which is not much of a compression.
It's not that simple. You also have to specify the effect set of the algorithm, meaning, assuming we do in place sort: every memory cell other that the input array are unchanged after termination. (If you return a fresh array, you have to specify something related). You also have to specify what happens for general sorting predicates, for example if the sorting predicate prints out the element it compares then this reveals (much of) the algorithm.
> The compression is stripping away the 'how'
The sorting example shows that this largely doesn't work in practise. In my experience for non-trivial programs you tend to have to carry around invariants whose complexity matches the size of the program you are verifying.
> I'm convinced that larger scale proof automation is way more essential than HoTT.
I strongly agree, but currently this proof automation is largely a hope, rather than a reality.
> crazy type hackery as seen in Haskell or Scala
Haskell and Scala have (local) type-inference. That makes those complex types (somewhat) digestible.
> dependent types just for refinement
If / when this really works well, so that you don't pay a price when you are not using complex types, then this would be very nice. I don't think PL technology is there yet. (I'm currently using a refinement typing approach in production code.)