4 ms·

> This separates programming from verification completely. This is simply not the case. Significant verification projects always plan for verification and do v

by darzu 11y ago

> This separates programming from verification completely. This is simply not the case. Significant verification projects always plan for verification and do verification in tandem. This is definitely true for all Dafny projects to date as well. Verification is just so much harder than unverified programming that you generally want to do everything you can while programming to make verification easier. This may become less true as proof automation improves but it will always be a tension. > But what makes you think you need dependent types to do full specification [...] ? Also, keep in mind that Dafny and similar tools can only express first order logic; this can significantly restricts the expressiveness of your specification language and intermediate lemmas. > program logic does not have to be constructive, instead you can use classical reasoning with excluded middle. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle (only NuPRL is I believe) so you can always assume it as an axiom if you'd like. Most projects don't do this because constructivism is a benefit not a burden in verification: it allows you to make distinctions that aren't possible in classical logic. I agree that Dafny and similar projects are very exciting though; Dafny's tight integration with Z3 provides an awesome level of automation that will keep getting better and better.

mafribe 11y ago
Significant verification projects always plan for verification and do verification in tandem. That may be the case, but the point is that dependently typed programming languages force you to verify every intermediate step, while program logic gives you the option to do so. A key problem in contemporary software engineering is that specifications constantly change (aka "customers don't know what they want"). Agile software engineering methodologies have mostly taken over from waterfalls because agile is designed from the start to minimise the cost of change (how successful they are at minimise the cost of change is another matter). If you have to redo not just the code itself and tests but also proofs every time your customer changes the spec, the costs of software development increase rapidly. Look at e.g. Java exception specifications, for a similar but much more benign problem. The program logic approach to verification does not force the full cost of verification on the programmer, because verification can be deferred until the program specification is stable and it's code passes all tests. This enables a hybrid approach to program correctness: in early states of the software engineering process, you use lightweight methods such as Hindley-Milner like typing systems, and testing, and only in later states you go for logic-based approaches. Let me repeat that the program logic approach always allows you to specify and verify from day one, so program logic gives you the best of both worlds. Dafny and similar tools can only express first order logic That's a design choice of Dafny's and orthogonal to dependent types vs program logic. Moreover, all program logics where observational completeness has been proven(which means you can prove exactly the program properties that are contextually observable) were based on first-order logic. This is a pretty good indication that higher-order is not needed for sheer expressivity. Higher-order logics are but a convenience that enables shorter specifications and proofs. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle It's a serious point. Look at the influential nominal approaches to handling bound names. The reason they were implemented in Isabelle and are heavily used there, but are basically not used in Coq, despite nominal techniques being perfectly constructive, is that nominal techniques have extremely short and uniform non-constructive proofs which can easily be handled by Isabelle's proof automation, while the corresponding constructive proofs are long, non-uniform and not easily handled by Coq's proof automation. The real reason everybody uses dependent types is that they are perfectly matched for the verification of pure functional programs, since proofs are pure functional programs. This is beautiful. But as soon as you want to verify non functional programs, that beautiful coincidence evaporates. This is another key shortcoming of the dependent types approach: it's unlikely that it can be extended in a beautiful way to low-level programming, stateful programming, timed programming, concurrent programming.

by darzu 11y ago

mafribe 11y ago

Significant verification projects always plan for verification and do verification in tandem. That may be the case, but the point is that dependently typed programming languages force you to verify every intermediate step, while program logic gives you the option to do so. A key problem in contemporary software engineering is that specifications constantly change (aka "customers don't know what they want"). Agile software engineering methodologies have mostly taken over from waterfalls because agile is designed from the start to minimise the cost of change (how successful they are at minimise the cost of change is another matter). If you have to redo not just the code itself and tests but also proofs every time your customer changes the spec, the costs of software development increase rapidly. Look at e.g. Java exception specifications, for a similar but much more benign problem. The program logic approach to verification does not force the full cost of verification on the programmer, because verification can be deferred until the program specification is stable and it's code passes all tests. This enables a hybrid approach to program correctness: in early states of the software engineering process, you use lightweight methods such as Hindley-Milner like typing systems, and testing, and only in later states you go for logic-based approaches. Let me repeat that the program logic approach always allows you to specify and verify from day one, so program logic gives you the best of both worlds. Dafny and similar tools can only express first order logic That's a design choice of Dafny's and orthogonal to dependent types vs program logic. Moreover, all program logics where observational completeness has been proven(which means you can prove exactly the program properties that are contextually observable) were based on first-order logic. This is a pretty good indication that higher-order is not needed for sheer expressivity. Higher-order logics are but a convenience that enables shorter specifications and proofs. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle It's a serious point. Look at the influential nominal approaches to handling bound names. The reason they were implemented in Isabelle and are heavily used there, but are basically not used in Coq, despite nominal techniques being perfectly constructive, is that nominal techniques have extremely short and uniform non-constructive proofs which can easily be handled by Isabelle's proof automation, while the corresponding constructive proofs are long, non-uniform and not easily handled by Coq's proof automation. The real reason everybody uses dependent types is that they are perfectly matched for the verification of pure functional programs, since proofs are pure functional programs. This is beautiful. But as soon as you want to verify non functional programs, that beautiful coincidence evaporates. This is another key shortcoming of the dependent types approach: it's unlikely that it can be extended in a beautiful way to low-level programming, stateful programming, timed programming, concurrent programming.