4 ms·

> Are there examples of cases where a system was very hard to verify with any one general technique, but much more practical to verify by using several domain-s

> Are there examples of cases where a system was very hard to verify with any one general technique, but much more practical to verify by using several domain-specific techniques and some kind of bridge between them I'm not sure what you mean by bridge but the halting problem comes to mind: the general case is impossible but you can prove common algorithms halt by showing they're structurally recursive (the recursive parameter always get smaller) or some metric always decreases on the recursive call (e.g. the sum of the length of two lists always gets smaller on the recursive call).

lmm 11y ago
> you can prove common algorithms halt by showing they're structurally recursive (the recursive parameter always get smaller) or some metric always decreases on the recursive call (e.g. the sum of the length of two lists always gets smaller on the recursive call) Right, but those are just special cases of the same technique - you can combined them by using dependent types to lift the list length to the type level and then this metric technique is just a special case of structural recursion.
- pron 11y ago
  Dependent types are not a verification technique. They are just one way of encoding statements about your program (in intuitionistic logic). The technique to prove those statement are either manual or manually-assisted (e.g. Coq), or automated using various model-checking algorithms (Liquid types). Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn't make verification any easier or harder. It's just a form of stating the properties you wish to verify.
  - lmm 11y ago
    Sure. What I'm saying is that you can encode statements about values and statements about types the same way, by using dependent types, and once you do that then you can verify halting of metric-recursive functions using exactly the same approach that you use to verify halting of structurally-recursive functions. So proving halting using a combination of proofs that metric-recursive functions halt and proofs that structurally-recursive functions halt isn't an example of it being useful to use two different approaches for different parts of the proof of correctness of a program, and doesn't make the case for having multiple approaches to verification and bridges between them.
    - pron 11y ago
      That depends on what you mean by "exactly the same approach". Can the same algorithm construct both proofs? Can it construct both proofs with the same computational complexity? If not, then you're not using the same approach. Using dependent types is more of a particular notation than a solution to verification. How you prove your type inference/checking is the hard part. Examples of approaches include SAT/SMT solvers, symbolic model checking, manual deduction, explicit model checking, abstract interpretation (which is really abstraction + explicit model checking; H-M inference algorithms can be described in terms of this approach), weakest preconditions, etc. You can use all of these approaches to infer/check dependent types, just as you can use them to verify program logic stated using means other than dependent types.
      - lmm 11y ago
        > That depends on what you mean by "exactly the same approach". Can the same algorithm construct both proofs? Can it construct both proofs with the same computational complexity? Yes, because once you're representing the values with dependent types, metric recursion and structural recursion are physically the same thing.
  - seanwilson 11y ago
    > Dependent types are not a verification technique...Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn't make verification any easier or harder. For what it's worth, every time I see articles and comments about the use of formal verification in general purpose programming around here, I never see any mention of how the actual verification part requires incredibly challenging manual proofs. In particular, I see articles about dependent types that give the impression you get the proofs for free when that isn't the case.
    - pron 11y ago
      Let me respond to that with a quote from "No Silver Bullet, Refired", by another Turing Award winner, Fred Brooks: > Even if "NSB" were universally seen as pessimistic, what is wrong with that? Is Einstein's statement that nothing can travel faster than the speed of light "bleak" or "gloomy?" How about Godel's result that some things cannot be computed? "NSB" undertakes to establish that "the very nature of software makes it unlikely that there will ever be any silver bullets." Turski, in his excellent response paper at the IFIP Conference, said eloquently: >> Of all misguided scientific endeavours, none are more pathetic than the search for the philosophers' stone, a substance supposed to change base metals into gold. The supreme object of alchemy, ardently pursued by generations of researchers generously funded by secular and spiritual rulers, is an undiluted extract of wishful thinking, of the common assumption that things are as we would like them to be. It is a very human belief. It takes a lot of effort to accept the existence of insoluble problems. The wish to see a way out, against all odds, even when it is proven that it does not exist, is very, very strong. And most of us have a lot of sympathy for these courageous souls who try to achieve the impossible. And so it continues. Dissertations on squaring a circle are being written. Lotions to restore lost hair are concocted and sell well. Methods to improve software productivity are hatched and sell very well. All too often we are inclined to follow our own optimism (or exploit the optimistic hopes of our sponsors). All too often we are willing to disregard the voice of reason and heed the siren calls of panacea pushers. > Turski and I both insist that pipe-dreaming inhibits forward progress and wastes effort. > So we come back to fundamentals. Complexity is the business we are in, and complexity is what limits us. R. L. Glass, writing in 1988, accurately summarizes my 1995 views: >> So what, in retrospect, have Parnas and Brooks said to us? That software development is a conceptually tough business. That magic solutions are not just around the corner. That it is timefor the practitioner to examine evolutionary improvements rather than to wait—or hope—for revolutionary ones. >> Some in the software field find this to be a discouraging picture. They are the ones who still thought breakthroughs were near at hand. >> But some of us—those of us crusty enough to think that we are realists—see this as a breath of fresh air. At last, we can focus on something a little more viable than pie in the sky. Now, perhaps, we can get on with the incremental improvements to software productivity that are possible, rather than waiting for the breakthroughs that are not likely to ever come. --- So discussing some methods of formal verification (such as manually checking dependent types) as a solution is like saying a particle accelerator is the solution to the alchemist's problem. Theoretically it can work; in practice, it's often too much effort :) Personally I'm not sure pipe-dreams inhibit forward progress, but they sure do generate a lot of noise...

lmm 11y ago

> you can prove common algorithms halt by showing they're structurally recursive (the recursive parameter always get smaller) or some metric always decreases on the recursive call (e.g. the sum of the length of two lists always gets smaller on the recursive call) Right, but those are just special cases of the same technique - you can combined them by using dependent types to lift the list length to the type level and then this metric technique is just a special case of structural recursion.

pron 11y ago
Dependent types are not a verification technique. They are just one way of encoding statements about your program (in intuitionistic logic). The technique to prove those statement are either manual or manually-assisted (e.g. Coq), or automated using various model-checking algorithms (Liquid types). Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn't make verification any easier or harder. It's just a form of stating the properties you wish to verify.
- lmm 11y ago
  Sure. What I'm saying is that you can encode statements about values and statements about types the same way, by using dependent types, and once you do that then you can verify halting of metric-recursive functions using exactly the same approach that you use to verify halting of structurally-recursive functions. So proving halting using a combination of proofs that metric-recursive functions halt and proofs that structurally-recursive functions halt isn't an example of it being useful to use two different approaches for different parts of the proof of correctness of a program, and doesn't make the case for having multiple approaches to verification and bridges between them.
  - pron 11y ago
    That depends on what you mean by "exactly the same approach". Can the same algorithm construct both proofs? Can it construct both proofs with the same computational complexity? If not, then you're not using the same approach. Using dependent types is more of a particular notation than a solution to verification. How you prove your type inference/checking is the hard part. Examples of approaches include SAT/SMT solvers, symbolic model checking, manual deduction, explicit model checking, abstract interpretation (which is really abstraction + explicit model checking; H-M inference algorithms can be described in terms of this approach), weakest preconditions, etc. You can use all of these approaches to infer/check dependent types, just as you can use them to verify program logic stated using means other than dependent types.
    - lmm 11y ago
      > That depends on what you mean by "exactly the same approach". Can the same algorithm construct both proofs? Can it construct both proofs with the same computational complexity? Yes, because once you're representing the values with dependent types, metric recursion and structural recursion are physically the same thing.
- seanwilson 11y ago
  > Dependent types are not a verification technique...Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn't make verification any easier or harder. For what it's worth, every time I see articles and comments about the use of formal verification in general purpose programming around here, I never see any mention of how the actual verification part requires incredibly challenging manual proofs. In particular, I see articles about dependent types that give the impression you get the proofs for free when that isn't the case.
  - pron 11y ago
    Let me respond to that with a quote from "No Silver Bullet, Refired", by another Turing Award winner, Fred Brooks: > Even if "NSB" were universally seen as pessimistic, what is wrong with that? Is Einstein's statement that nothing can travel faster than the speed of light "bleak" or "gloomy?" How about Godel's result that some things cannot be computed? "NSB" undertakes to establish that "the very nature of software makes it unlikely that there will ever be any silver bullets." Turski, in his excellent response paper at the IFIP Conference, said eloquently: >> Of all misguided scientific endeavours, none are more pathetic than the search for the philosophers' stone, a substance supposed to change base metals into gold. The supreme object of alchemy, ardently pursued by generations of researchers generously funded by secular and spiritual rulers, is an undiluted extract of wishful thinking, of the common assumption that things are as we would like them to be. It is a very human belief. It takes a lot of effort to accept the existence of insoluble problems. The wish to see a way out, against all odds, even when it is proven that it does not exist, is very, very strong. And most of us have a lot of sympathy for these courageous souls who try to achieve the impossible. And so it continues. Dissertations on squaring a circle are being written. Lotions to restore lost hair are concocted and sell well. Methods to improve software productivity are hatched and sell very well. All too often we are inclined to follow our own optimism (or exploit the optimistic hopes of our sponsors). All too often we are willing to disregard the voice of reason and heed the siren calls of panacea pushers. > Turski and I both insist that pipe-dreaming inhibits forward progress and wastes effort. > So we come back to fundamentals. Complexity is the business we are in, and complexity is what limits us. R. L. Glass, writing in 1988, accurately summarizes my 1995 views: >> So what, in retrospect, have Parnas and Brooks said to us? That software development is a conceptually tough business. That magic solutions are not just around the corner. That it is timefor the practitioner to examine evolutionary improvements rather than to wait—or hope—for revolutionary ones. >> Some in the software field find this to be a discouraging picture. They are the ones who still thought breakthroughs were near at hand. >> But some of us—those of us crusty enough to think that we are realists—see this as a breath of fresh air. At last, we can focus on something a little more viable than pie in the sky. Now, perhaps, we can get on with the incremental improvements to software productivity that are possible, rather than waiting for the breakthroughs that are not likely to ever come. --- So discussing some methods of formal verification (such as manually checking dependent types) as a solution is like saying a particle accelerator is the solution to the alchemist's problem. Theoretically it can work; in practice, it's often too much effort :) Personally I'm not sure pipe-dreams inhibit forward progress, but they sure do generate a lot of noise...