>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.