3 ms·

> Dependent types rely on deductive proofs for verification, and deductive proofs (the "proof theory" part of a logic) are the least scalable verification metho

> Dependent types rely on deductive proofs for verification, and deductive proofs (the "proof theory" part of a logic) are the least scalable verification method as they are least amenable to automation. What? You can generate proofs for the trivial cases using various algorithms like constraint solving. Things like sledgehummer tactic, omega tactic, the whole F* language simply prove you wrong (by construction ;) You need to prove manually only complex cases, where your constrain solver would not manage to generate the proof. > But now I claim that their composition `foo bar` never crashes (on `head`) If you proved that foo does not crashes on head for any predicate P and any integer X, and bar terminates, than foo bar terminates. What's the problem? > The idea that properties compose and that you can cheaply reuse knowledge about components to prove stuff about their composition is just mathematically false. There are a couple of results I mention in my blog posts that show that. Could you refer to the proof of that, as well as give the definition of ``cheaply'' and especially the evidence that a composition of lemmas and theorems would be more expensive than a constraint solvers-based methods? I didn't state that proving is easy or cheap, just that manual proving with a usage of constraint solvers for trivial cases is more scalable and makes more sense for sufficiently big programs.

9q9 7y ago
Aside: Sledgehammering doesn't currently work in Curry-Howard-based provers. (This may change in the future, it's an active research topic.)
- ernst_klim 7y ago
  I was talking about deductive proving, not constructive in particular.
pron 7y ago
> What? You can generate proofs for the trivial cases using various algorithms like constraint solving. Things like sledgehummer tactic, omega tactic, the whole F* language simply prove you wrong I don't understand this simple proof. How does allowing some automation prove that it's not the method least amenable to automation? > If you proved that foo does not crashes on head for any predicate P and any integer X, and bar terminates, than foo bar terminates. What's the problem? Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense. Clearly, the important correctness properties of your program arise from the composition of all components of your program (or you wouldn't need them). If the same correctness property arises from each component in isolation, then you wouldn't need all others. Most correctness properties are just not compositional (inductive), and the belief that a non-compositional property can be proven by combining results about the components at a cost that scales with their number (polynomially, exponentially -- take your pick) is mathematically false. > Could you refer to the proof of that, as well as give the definition of ``cheaply'' and especially the evidence that a composition of lemmas and theorems would be more expensive than a constraint solvers-based methods? I never mentioned "constraint solvers-based methods" (and I'm not even sure what you're referring to [1]). Once you need to prove something, the method is irrelevant, and the theoretical limitations kick in. Showing that one method is easier or harder for instances encountered in practice requires empirical research, so I can't say whether their harder or easier, just that so far deductive proofs are the least scalable in practice. Finally, I can say that we cannot in general decompose correctness to make it easier. Some relevant results are in the papers mentioned in my post in the sections "Correctness does not decompose" and "Language abstractions cannot generally be exploited". [1]: Perhaps you're referring to SMT solvers and the like, but they are rarely used in isolation. They are used as components in deductive proofs, model checkers and concolic tests. As usual, they are more effective when used in the latter two than in the first.
- ernst_klim 7y ago
  > Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense. What? If foo terminates and bar terminates, than foo bar clearly terminates. How does this make no sense? > Most correctness properties are just not compositional (inductive), and the belief that a non-compositional property can be proven by combining results about the components at a cost that scales with their number (polynomially, exponentially -- take your pick) is mathematically false. Ok, let's check your blog and what paper you mention > A Parametric Analysis of the State-Explosion Problem in Model Checking⋆ What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale. What this foobar example has to do with this tho? Foo does not terminate due to exception, and so does Foo Bar. How doesn't this compose? > I don't understand this simple proof. How does allowing some automation prove that it's not the method least amenable to automation? Because you can automate anything you can prove with a SMT or model checker?
  - pron 7y ago
    > How does this make no sense? Because most correctness properties aren't compositional. > What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale. No, you've misunderstood the paper, and missed the part of the post where I provide necessary context. Like a lot of work in computational complexity theory, they're referring to the model checking problem, i.e. the problem of determining whether a program satisfies some property, not to any particular verification algorithm. Their results apply to all methods (their proofs don't not rely on any particular verification method but show hardness results). Also, it's funny that you say "they don't scale." You're right, none of the formal methods we have scales nearly as well as we'd like, to the point we can say "they don't scale" [1]. Of them, the one that scales the least is deductive proofs. That's the main reason it's the formal methods that is used the least. > constraint based solutions I don't know what you mean by that (SMT?), and I don't recall mentioning those. > Because you can automate anything you can prove with a SMT or model checker? Yes, model checkers are completely automatic. SMT is a class of algorithms and techniques used in various verification methods -- deductive proofs, model checking, static analysis, concolic testing -- not a verification method in itself, so I'm not sure what you mean exactly. Sometimes they're used to prove some logical proposition directly, but they're not used as a complete software verification tool, because they're rather limited on their own. [1]: When applied to the code directly. We have ways of scaling formal methods by verifying high level specifications.

9q9 7y ago

Aside: Sledgehammering doesn't currently work in Curry-Howard-based provers. (This may change in the future, it's an active research topic.)

ernst_klim 7y ago
I was talking about deductive proving, not constructive in particular.

pron 7y ago

> What? You can generate proofs for the trivial cases using various algorithms like constraint solving. Things like sledgehummer tactic, omega tactic, the whole F* language simply prove you wrong I don't understand this simple proof. How does allowing some automation prove that it's not the method least amenable to automation? > If you proved that foo does not crashes on head for any predicate P and any integer X, and bar terminates, than foo bar terminates. What's the problem? Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense. Clearly, the important correctness properties of your program arise from the composition of all components of your program (or you wouldn't need them). If the same correctness property arises from each component in isolation, then you wouldn't need all others. Most correctness properties are just not compositional (inductive), and the belief that a non-compositional property can be proven by combining results about the components at a cost that scales with their number (polynomially, exponentially -- take your pick) is mathematically false. > Could you refer to the proof of that, as well as give the definition of ``cheaply'' and especially the evidence that a composition of lemmas and theorems would be more expensive than a constraint solvers-based methods? I never mentioned "constraint solvers-based methods" (and I'm not even sure what you're referring to [1]). Once you need to prove something, the method is irrelevant, and the theoretical limitations kick in. Showing that one method is easier or harder for instances encountered in practice requires empirical research, so I can't say whether their harder or easier, just that so far deductive proofs are the least scalable in practice. Finally, I can say that we cannot in general decompose correctness to make it easier. Some relevant results are in the papers mentioned in my post in the sections "Correctness does not decompose" and "Language abstractions cannot generally be exploited". [1]: Perhaps you're referring to SMT solvers and the like, but they are rarely used in isolation. They are used as components in deductive proofs, model checkers and concolic tests. As usual, they are more effective when used in the latter two than in the first.

ernst_klim 7y ago
> Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense. What? If foo terminates and bar terminates, than foo bar clearly terminates. How does this make no sense? > Most correctness properties are just not compositional (inductive), and the belief that a non-compositional property can be proven by combining results about the components at a cost that scales with their number (polynomially, exponentially -- take your pick) is mathematically false. Ok, let's check your blog and what paper you mention > A Parametric Analysis of the State-Explosion Problem in Model Checking⋆ What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale. What this foobar example has to do with this tho? Foo does not terminate due to exception, and so does Foo Bar. How doesn't this compose? > I don't understand this simple proof. How does allowing some automation prove that it's not the method least amenable to automation? Because you can automate anything you can prove with a SMT or model checker?
- pron 7y ago
  > How does this make no sense? Because most correctness properties aren't compositional. > What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale. No, you've misunderstood the paper, and missed the part of the post where I provide necessary context. Like a lot of work in computational complexity theory, they're referring to the model checking problem, i.e. the problem of determining whether a program satisfies some property, not to any particular verification algorithm. Their results apply to all methods (their proofs don't not rely on any particular verification method but show hardness results). Also, it's funny that you say "they don't scale." You're right, none of the formal methods we have scales nearly as well as we'd like, to the point we can say "they don't scale" [1]. Of them, the one that scales the least is deductive proofs. That's the main reason it's the formal methods that is used the least. > constraint based solutions I don't know what you mean by that (SMT?), and I don't recall mentioning those. > Because you can automate anything you can prove with a SMT or model checker? Yes, model checkers are completely automatic. SMT is a class of algorithms and techniques used in various verification methods -- deductive proofs, model checking, static analysis, concolic testing -- not a verification method in itself, so I'm not sure what you mean exactly. Sometimes they're used to prove some logical proposition directly, but they're not used as a complete software verification tool, because they're rather limited on their own. [1]: When applied to the code directly. We have ways of scaling formal methods by verifying high level specifications.