blog

uicksort in Idris as in Java, but then the program will not serve as proof of its correctness). I think that the claim that with what we know how to do today producing the former is as easy as the latter, let alone easier, requires some empirical evidence. [1]: https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris

y allow you to state program properties formally, and then use either (expensive) formal proofs or weaker forms of verification (like generated tests) to verify them. Proofs are both extremely costly and are very rarely a requirement; their added confidence beyond other, weaker, but far cheaper, forms of verification is very rarely worth their tremendous cost. [0]: See this example of a simplified Quicksort in Idris: https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris [1]: End-to-end verification is ensuring that global correctness properties (e.g., "the database is always consistent", or "no user ever gets access to another's data") are preserved all the way to source code or even to machine-code. Most "formally verified" software, at least in industry, isn't verified end-to-end. Rather, either global properties are verified not against the code but a high-level description of the software or only local properties are verified at the code level, or both (but with a gap).

"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