> Indeed, which is why I think something like Idris will probably be the future.
I very much doubt it. I think other code-level specification languages (like JML for Java or ACSL for C), are much better suited to the configurable level of verification that you're looking for. The reason their tooling[1] is better than Idris's is not just because they're more mature, but for deeper reasons, too.
While working in different formalisms (dependent types or direct logic) doesn't make much of a difference, when you specify in types, the lowest level of confidence you allow is formal proof, which, as you note, is beyond reach for anything but small and simple code. It doesn't make much of a difference whether you need to prove a JML specification or an Idris type, but a JML specification allows you to optionally use weaker but much cheaper forms of verification like concolic testing, regular test generation etc.
OTOH, Idris already has test-generation libraries that require yet another form of specification, just because types won't work with anything less than proof. I heard you could achieve the same with types, but that requires enclosing the weakly-verified types in monads, so type T and type `Weak T` is not the same.
Idris is one of many (I've lost count) of experiments in code-level formal verification. So far I don't see any indication it is closer to being "the future" than any of the multitude of other experiments. I don't think it's necessarily worse, either (while suffering from the problem I mentioned above, I assume it has advantages, too), but right now if you hear a lot about Idris it mostly means you hang around Haskellers, who have taken a liking to the language because of its similarity to Haskell in both spirit and style.
> It doesn't make much of a difference whether you need to prove a JML specification or an Idris type, but a JML specification allows you to optionally use weaker but much cheaper forms of verification like concolic testing, regular test generation etc.
I think you're overshooting the target I was aiming at. You can use simple algebraic types in Idris and check your invariants dynamically as you would in any less expressive language, then incrementally move some of these to statically checked invariants where feasible.
Specification-tools require a lot more work in separate specification languages, which are often unwieldy.
> if you hear a lot about Idris it mostly means you hang around Haskellers, who have taken a liking to the language because of its similarity to Haskell in both spirit and style.
To some extent that's true. So take Haskell, remove the default lazy evaluation which trips so many people up, remove all the restrictions around types since it supports full dependent typing (no more whacky type trickery to check some invariants statically!), support for syntax extensions to support EDSLs, and easy integration with C. Welcome to Idris.
Frankly, this is pretty much the full wishlist that advanced programmers have been wanting for years, and I've seen a lot of interest in Idris since its recent 1.0 release.
> You can use simple algebraic types in Idris and check your invariants dynamically as you would in any less expressive language, then incrementally move some of these to statically checked invariants where feasible.
That simply means writing less specifications, or writing specifications in two different ways. Spec languages allow you to decouple the specification from the verification effort. You write some specs (or not), and then you decide whether you want to prove them, generate tests, add assertions etc.
> Specification-tools require a lot more work in separate specification languages, which are often unwieldy.
They require exactly the same amount of work (whether you write your spec using types or logic doesn't make a difference; the specs are the same), and the language is mostly the object language (i.e. the programming language) with the addition of some quantifiers. The result is usually not much different than a language with a rich type system.
> Frankly, this is pretty much the full wishlist that advanced programmers have been wanting for years, and I've seen a lot of interest in Idris since its recent 1.0 release.
I think this is the wishlist of programmers who like Haskell... Formal methods people don't agree at all that this is the future.
> Spec languages allow you to decouple the specification from the verification effort.
I think the recorded history of comments drifting from source code proves that this isn't likely to work. The properties to verify should be expressed within the same code so they must evolve together.
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.
> I think this is the wishlist of programmers who like Haskell... Formal methods people don't agree at all that this is the future.
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.
And of course, you're probably still thinking that verification efforts would only be applied when absolutely necessary, because of the inherent cost, where I'm foreseeing a future where some verification is part of most programmers' workflow, not just high assurance systems, and the cost for some common set of verification efforts are low and standardized.
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.
> 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.
If Idris (or a language like it) turns out to be significantly valuable in practice, I don't believe it will be thanks to its ability to formally prove deep correctness properties, for the reasons I gave above (as code-level specification languages do a better job of it), but because it may turn out that proving some weaker correctness properties (that don't quite reach the bar of formal verification but that exceed what's possible with weak type systems like Haskell's) empirically turns out to yield a significant improvement in correctness for a reasonable amount of effort. I certainly cannot dismiss such a possibility, but I don't think this is something anyone can foresee. It either empirically turns out to be the case or not.
> 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.
> 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.
> 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.
They require no more discipline than remembering to run your unit tests in your build. History has shown that people -- even ordinary programmers -- have come to incorporate their unit tests into their build so that they run automatically. A much, much bigger challenge would be to get programmers to write specifications in the first place -- whether in types or in logic.
> Firstly, you don't always, given type inference.
Those types that type inference can infer correspond to specs that automated tools prove. The algorithms are even the same.
> 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.
Whether you write your proofs using dependent types or using logic, the process is identical, and in either case it is so laborious that no one has been able to do it for large programs anyway, not before, not during and not after.
> You now have a mashup of formal properties with uncertain failure modes.
1. Those are not the same failure modes. 2. Welcome to the world of formal methods. Again, full proof of large programs has never been accomplished. We who use formal methods in real-world projects must use a mashup of techniques of various confidence levels.
> 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.
You sound like someone quoting something rather than a practitioner of formal methods. We use a plethora of tools, each contributing something to the confidence. We have no choice given that formal proof is beyond our reach for the properties that we must verify.
> They're writing everything in the same language, not different languages using different compilers and different tools.
No, those are different tools (compiler and test tool) and different languages (type level and object level; yes they use the same syntax, but code-level spec also does.
> Right, because dependent types typically leak too much of their implementation due to the properties that must be satisfied.
Dependent types are just a formalism for writing specifications. The problem is what kind of verification is done, and types require proof.
> Idris' syntactic support can then make this easy for library clients to use correctly.
No one has ever been able to make formal proofs even moderately hard, let alone easy. Maybe Idris will perform this miracle, but my bet is on other formal verification techniques. I am not aware of any formal methods researcher who believes that formal proofs will become affordable for mainstream software using any of the formal proof techniques we currently have.
> 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 someone who actually uses formal methods, I know what's been done and what's only been claimed in research. Lightweight static capabilites are not really formal methods; their tokens for runtime assertions. They're cool (and have been used in OOP languages since long before that paper), but they're something else altogether.
> because what are types if not a form of code-level specification?
That's right, but they're specs that settle for no weaker form of verification than proof.
> Code-level specifications that are not types tend to be fairly non-compositional...
Huh? It's just a different formalism. They behave the same, and require the same discipline. The only difference is that they don't necessarily require proof.
> 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.
Session types are really weak, and can't actually verify interesting protocols. That resources are cleaned is a local property that doesn't fall in the category we're discussing (and can be achieved without formal methods at all). That a general ledger is always balanced -- well, that's a correctness property that I'd like to see someone prove in Idris in a real, large distributed system. It's never been successfully done.
> These are relatively simple properties for which we now have good, reusable abstractions
What we don't know is what is the relationship between having such weak guarantees and actual software correctness.
I very much doubt it. I think other code-level specification languages (like JML for Java or ACSL for C), are much better suited to the configurable level of verification that you're looking for. The reason their tooling[1] is better than Idris's is not just because they're more mature, but for deeper reasons, too.
While working in different formalisms (dependent types or direct logic) doesn't make much of a difference, when you specify in types, the lowest level of confidence you allow is formal proof, which, as you note, is beyond reach for anything but small and simple code. It doesn't make much of a difference whether you need to prove a JML specification or an Idris type, but a JML specification allows you to optionally use weaker but much cheaper forms of verification like concolic testing, regular test generation etc.
OTOH, Idris already has test-generation libraries that require yet another form of specification, just because types won't work with anything less than proof. I heard you could achieve the same with types, but that requires enclosing the weakly-verified types in monads, so type T and type `Weak T` is not the same.
Idris is one of many (I've lost count) of experiments in code-level formal verification. So far I don't see any indication it is closer to being "the future" than any of the multitude of other experiments. I don't think it's necessarily worse, either (while suffering from the problem I mentioned above, I assume it has advantages, too), but right now if you hear a lot about Idris it mostly means you hang around Haskellers, who have taken a liking to the language because of its similarity to Haskell in both spirit and style.
[1]: See here for an example of some automated JML tools http://www.openjml.org/, and here for semi-automated tools (using proof assistants) http://krakatoa.lri.fr/