> But they are. Remember, those specifications are continually verified against the code, either as proofs, tests, automated proofs, etc..
They are not though, they require separate steps using separate tools. These steps are not guaranteed to be taken, they require discipline, time and process, and history has shown that steps with those requirements are only taken when absolutely necessary, not as a matter of course.
You've argued that people already do this, but I submit that only those people already doing difficult verification already do this, which are not the people I'm talking about. I'm talking about ordinary programmers doing verification, where they can, as part of normal programming.
> Specification and verification are always separate steps. [...] You write types/specs, then you need to prove them.
Firstly, you don't always, given type inference.
Secondly, programmers writing a program don't consider themselves to be writing proofs, that's my point. The proof just follows naturally from reasoning about the semantics of the code as they're writing it, not later when they have to go back and read it who-knows-how-much-later, and then figure out what conditions they should try to verify.
Regarding pluggable verification, I'm not sold. You now have a mashup of formal properties with uncertain failure modes. Look at the work on RustBelt [1] to see how easily naive composition can break important safety assumptions.
[1] http://lambda-the-ultimate.org/node/5448
> Your tests aren't run by the compiler, yet people plug them into their build process.
Tests aren't a meaningful form of verification; they can't prove the absence of bugs, only their presence. Rarely is a property verifiable by exhaustive case tests.
> People specify those properties they want to verify with proofs using types, and they specify them in a different way when they want to verify them with automated test generation. That doesn't seem like a convergence to me.
They're writing everything in the same language, not different languages using different compilers and different tools. They can't run their program until their verification succeeds, because the program has no meaning without verification. That's pretty convergent compared to alternatives.
> On the other hand, no one -- even teams of Phd students -- has ever been able to write a program larger than 10KLOC that's verified at the same confidence level provided by dependent types, and those few programs were not only short, but heavily simplified.
Right, because dependent types typically leak too much of their implementation due to the properties that must be satisfied.
I think the interest in EDSLs show a way forward though, because verifying small programs is sometimes difficult but often feasible, and domain-specific languages can often be reduced to some simple kernels with some readily verifiable properties. Idris' syntactic support can then make this easy for library clients to use correctly.
Of course, you can suggest this is all speculative, but it's not pie-in-the-sky as you've been claiming. People have been doing this for years already, with both dependent and ordinary type systems (see Oleg's lightweight static capabilities).
> (as code-level specification languages do a better job of [proving deep correctness properties])
I'm frankly still confused by your position on this, because what are types if not a form of code-level specification? Code-level specifications that are not types tend to be fairly non-compositional, have few means of abstraction and reuse, and as I mentioned earlier, require extra discipline.
Finally, I never actually claimed that Idris is or will be some "final solution" to software verification. As I initially said, and later reiterated, we need to be able to incrementally move the line towards or away from full verification as feasibility dictates, during ordinary programming, which something like Idris permits. Certainly Idris may be too expressive, and something like dependent Haskell might strike a better balance in the end, but Idris strikes a decent balance and exists right now.
> I really wish some of the people who think Idris is the future would actually try using it to prove some properties of a tiny, 5-line quicksort algorithm -- say, that it actually sorts and that it runs in worst-case quadratic complexity.
These aren't the typical properties you want to verify in most software, so I'm not sure what you think this proves. More typical properties are the correctness of protocols, for which we might use session types, that a general ledger is always balanced, that resources are always cleaned up and so don't take down your service, and so on.
These are relatively simple properties for which we now have good, reusable abstractions, not sophisticated control-flow dependent properties you need to specify and verify all in one place as with quicksort.