8 ms·

> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations It would be great if yo

> The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations It would be great if you've mentioned them and briefly described why are they limiting. > model checking Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible. I would argue that proving stuff manually using SMT for trivial cases, as F* does, would be much more productive than doing the whole proof using any sort of constrain solver (if this would ever work for a sufficiently big program). The main problem of a constrain solvers is that they don't scale well. When you proved lemmas for a small block of code, you simply reuse those for higher order proofs. Constraints are being accumulated (tho not linearly) when the program grow and so does its state.

pron 7y ago
> It would be great if you've mentioned them and briefly described why are they limiting. I've done so here: https://news.ycombinator.com/item?id=20714845 https://news.ycombinator.com/item?id=20714845 > Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible. The same is true for deductive proofs, of which dependent types are a particular instance, only the problem is far worse. It is true that there are cases where deductive proofs are more feasible than model checking, but the converse is true in a much wider portion of cases. That's why deductive proofs are rarely the first choice, and they're used selectively, usually only after other methods have failed. Overall, deductive proof, although it certainly has its place in certain circumstances, is the least scalable verification method we have. This means that it's the last method you want to use by default, let alone bake it into your type system. > Constraints are being accumulated (tho not linearly) when the program grow and so does its state. This is true regardless of the verification method used. See my blog post here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity > When you proved lemmas for a small block of code, you simply reuse those for higher order proofs. No, you can't "simply" reuse results. Here's an example (given in the post in Java, my preferred language, but as this is a post about Haskell, let me show it in Haskell): foo :: (Integer -> Bool) -> Integer -> Integer foo p x | x <= 2 || odd x = 0 | otherwise = head [i | i <- [x, x-1 .. 1], (p i) && p (x - i)] bar :: Integer -> Bool bar x = null [1 | i <- [x-1, x-2 .. 2], s <- [x, x-i .. 0], s == 0] These two subroutines are very simple, clearly terminating, and you can easily prove almost any property of interest about each of them in isolation. But now I claim that their composition `foo bar` never crashes (on `head`); can you prove me right or wrong? Feel free to "simply" reuse any proof about any of them. 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. We know that if you have a composition of components X_1 ∘ ... ∘ X_n then the cost of verifying some property of their composition is not only not polynomial in n, it's not even exponential in n (it's not any computable function in n, I think). I.e. it is a mathematical result that you cannot, generally, hide the complexity of components to make verification of their compsition scale with their number.
- ernst_klim 7y ago
  > 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.
9q9 7y ago
As far as I understand -- please correct me if I'm wrong -- F* uses dependent types as a foundation of maths (i.e. a logic) and embeds program logic via a HTT (= Hoare Type Theory). This is a very nice division of labour between programming and verification.

pron 7y ago

> It would be great if you've mentioned them and briefly described why are they limiting. I've done so here: https://news.ycombinator.com/item?id=20714845 https://news.ycombinator.com/item?id=20714845 > Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible. The same is true for deductive proofs, of which dependent types are a particular instance, only the problem is far worse. It is true that there are cases where deductive proofs are more feasible than model checking, but the converse is true in a much wider portion of cases. That's why deductive proofs are rarely the first choice, and they're used selectively, usually only after other methods have failed. Overall, deductive proof, although it certainly has its place in certain circumstances, is the least scalable verification method we have. This means that it's the last method you want to use by default, let alone bake it into your type system. > Constraints are being accumulated (tho not linearly) when the program grow and so does its state. This is true regardless of the verification method used. See my blog post here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity > When you proved lemmas for a small block of code, you simply reuse those for higher order proofs. No, you can't "simply" reuse results. Here's an example (given in the post in Java, my preferred language, but as this is a post about Haskell, let me show it in Haskell): foo :: (Integer -> Bool) -> Integer -> Integer foo p x | x <= 2 || odd x = 0 | otherwise = head [i | i <- [x, x-1 .. 1], (p i) && p (x - i)] bar :: Integer -> Bool bar x = null [1 | i <- [x-1, x-2 .. 2], s <- [x, x-i .. 0], s == 0] These two subroutines are very simple, clearly terminating, and you can easily prove almost any property of interest about each of them in isolation. But now I claim that their composition `foo bar` never crashes (on `head`); can you prove me right or wrong? Feel free to "simply" reuse any proof about any of them. 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. We know that if you have a composition of components X_1 ∘ ... ∘ X_n then the cost of verifying some property of their composition is not only not polynomial in n, it's not even exponential in n (it's not any computable function in n, I think). I.e. it is a mathematical result that you cannot, generally, hide the complexity of components to make verification of their compsition scale with their number.

ernst_klim 7y ago
> 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.

9q9 7y ago

As far as I understand -- please correct me if I'm wrong -- F* uses dependent types as a foundation of maths (i.e. a logic) and embeds program logic via a HTT (= Hoare Type Theory). This is a very nice division of labour between programming and verification.