> The properties to verify should be expressed within the same code so they must evolve together.

But they are. Remember, those specifications are continually verified against the code, either as proofs, tests, automated proofs, etc..

> If specification and verification are a separate step, those steps may not happen at all because the program will run without them. Verification must be part of the normal workflow of expressing a program and getting it running, or it just won't happen.

Specification and verification are always separate steps. You write tests, then you need to run them. You write types/specs, then you need to prove them. If you're concerned that the verification isn't done by the compiler, then that's the whole point. You want the verification to be pluggable, otherwise, you're limited to unaffordable formal proofs. As to "it just wouldn't happen", this is exactly how people using formal specification today do it; in fact, everybody does it. Your tests aren't run by the compiler, yet people plug them into their build process.

> If you see specification and verification as separate problems from programming, then it seems only natural to see a divergence down the road and not a convergence.

Specification and verification must be separate, or you'll need to write a new spec depending on how you want it to be verified. Indeed, this is how it's done in Idris. 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.

> We're already part way there with the pervasive use of static type systems, and the work on refinement typing, as in Liquid Types, brings us even closer.

If you think that the use of dependent types even remotely resembles the use of inferred types, then I don't think you have much experience with formal methods, and dependent types do take you from the realm of programming into the realm of formal methods. It's like saying that we're part way to a particle accelerator in every home thank's to the pervasive use of microwave ovens. Just to give you a sense of the difference, people have been writing ever growing, complex, and working programs in typed languages for at least 50 years now. 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. If you watch talks by Xavier Leroy, one of the world's premier experts on this particular form of verification (semi-manual, deductive end-to-end verification), you see that even he says that the approach doesn't scale in general to beyond a few hundred to about a thousand lines of code.

Idris -- like the scores of others of formal methods projects out there -- is an experiment in one particular approach. It's not a step towards some future (other than in the important research sense), because no one in the formal methods community has any idea what form the future of formal methods will take. 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. Here is a solution to the first part[1], and this is for a pretty trivial 5-line algorithm. How many developers can do that, do you think? All I know is that no one can do that for programs that aren't small and simple. Thankfully, this form of verification is not the only tool in the formal methods toolbox, but I really find it hard to be convinced that this way is the future.

[1]: https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris