4 ms·

>Also, I don't think that engineers are necessarily interested in proof, Depends on the area the engineer works in. Starting from some cost of failure you actu

>Also, I don't think that engineers are necessarily interested in proof, Depends on the area the engineer works in. Starting from some cost of failure you actually want a proper proof, because the inherent chance of error in incomplete induction becomes unacceptable. >Because if the logic is sound and something is true in the model, You can perfectly formalize this model using dependent types and use it there, don't you? > So the reality is that we have no idea how to verify programs that aren't tiny Yeah, I know, our brains are to small to properly verify everything, and we need to find ways to outsource as much as possible to machines. Doesn't mean we need to willfully embrace blind faith in incomplete induction.

pron 7y ago
> Depends on the area the engineer works in. Sure, but let's say that it's a conservative estimate that 99% don't need proofs. I acknowledged in the beginning that deductive proofs have a place in some niches. > You can perfectly formalize this model using dependent types and use it there, don't you? The logic is already a formalization of the model. Yet finding a counterexample in the model directly is very often easier than finding a deductive proof in the logic. Some people got a Turing award for that discovery. > Doesn't mean we need to willfully embrace blind faith in incomplete induction. Formal methods is not "blind faith". Second, we haven't willfully given up on deductive proofs; it's just that for decades we've tried to scale them and couldn't, so out of necessity we found methods that have worked better in practice. I don't know if 200 years from now people won't be able to make deductive proofs feasible, but why not use formal methods to make our software better and cheaper now? In any event, all I want is for people to know (what formal methods research and practice already does) that software correctness is an extremely complex topic, with severe challenges that are both theoretical and practical, and anyone who suggests that there is a known specific solution to the problem or that one of the many imperfect avenues we're exploring is "the future", doesn't know what they're talking about.
- permeakra 7y ago
  >Sure, but let's say that it's a conservative estimate that 99% don't need proofs 99% don't need formal verification, they are OK with unit tests. If one is actually that concerned with an effort to perform actual verification, they most likely want an actual proof. >The logic is already a formalization of the model. So? >it's just that for decades we've tried to scale them and couldn't, For decades people didn't care for formal verification. Absolute majority of 'engineers' don't see any use in it. You, on the other hand, see little use for formal verification with dependent types. Well, forgive me for drawing a parallel here. I want some specific guarantees that are fairly easy to express and keep track with dependent types, not some fancy offshot of Hoare logic. Why would I care for a method clearly inferior for my use cases? == Let's return a bit and examine one specific case again. Consider situation: one writes a generic merge-join function over sorted arrays. There, input arrays must sorted with same predicate over same, possibly virtual, key. To express this in specification on the input data one need to - quantify over the types of both arrays - quantify over the type of the key - and all the functions able to produce a key of this type from elements of array 1 - and all the functions able to produce a key of this type from elements of array 2 - quantify over the ordering predicate over values of the key type - express that ordering holds for each pair of elements of the array -- i.e. quantify over indicies of arrays 1 and 2. - For which one needs information on index bonds attached to arrays I can, with some effort, express it in the language of type theory. I'm very interested how one can express it using, say, first order logic that, you know, doesn't allow for quantification over predicates.
  - pron 7y ago
    > 99% don't need formal verification, they are OK with unit tests. Formal verification can be cheaper than tests. It's not just about a higher confidence, but also about achieving similar confidence more cheaply. That's one of the reasons why deductive proofs are not so popular in formal methods research -- they're too inflexible. > If one is actually that concerned with an effort to perform actual verification, they most likely want an actual proof. But we don't need to hypothesize -- they don't. Almost all formal verification in industry uses model checkers and sound static analysis. If you are interested in addressing the needs of certain small niches, that's one thing, but the thrust of formal methods research is about helping as much software as possible, and so deductive proofs are not the focus, because they're well behind other methods. > So? So, if you have a model checker, you don't need to write a proof. The model-checker could automatically provide a model-theoretical proof for you, at the press of a button. That's how, say, avionics software is verified. That's how Intel's chips are verified. People can't afford to write proofs for that volume of software. People write proofs only when model checking fails, or to tie together model checking results. It's no one's first choice (unless they're researchers or hobbyists). > For decades people didn't care for formal verification. It doesn't seem like you're familiar with the field. There was a huge boost in formal methods in the 70s followed by a research winter when people over promised and underdelivered. Then, about 20 years ago, there was a resurgence with different goals. In general, research now focuses on managing cost vs. benefit, reducing certain kinds of bugs, and finding ways to make verifiation more flexible, as we've so far been unable to make end-to-end verification scale. > Why would I care for a method clearly inferior for my use cases? I don't understand why you think it's inferior. It is absolutely not, and it is superior where it matters most. Expressiveness is the same, so specification is the same, but verification is flexible. You can use deductive proofs, or verifiation methods that have shown more promise. > I'm very interested how one can express it using, say, first order logic that, you know, doesn't allow for quantification over predicates. What? Of course FOL allows quantification over predicates and functions if they are elements of the domain, as they are in say, set theory (in fact, there is an assumption at the base of modern logic, that any mathematical theory could be expressed in some first-order language). Or, you could use HOL, if you like. But again, the theory is not the problem here. It's the chosen verification tool (and BTW, formal methods practitioners normally prefer to weaken the specification power if it reduces the cost of verification). Your example, in particular, is easily expressed in FO set theory, or many kinds of many-sorted FOL, or in HOL. For example, ∀ K, V . ∀ f ∈ K → V . ... is a trivial, perfectly normal, first-order logic over sets. In fact, dependent type theories like Lean's strive to be interpretable in set theory. But really, the choice theory is the least important issue with dependent types or software verification in general. If you are, however, interested in theory (as I am), you can read my series on TLA+. It is a first-order logic that is strictly richer and more expressive than lambda-calculus-based dependent type theories (unless you deeply embed it in them, and describe your computations in monads): https://pron.github.io/tlaplus https://pron.github.io/tlaplus

pron 7y ago

> Depends on the area the engineer works in. Sure, but let's say that it's a conservative estimate that 99% don't need proofs. I acknowledged in the beginning that deductive proofs have a place in some niches. > You can perfectly formalize this model using dependent types and use it there, don't you? The logic is already a formalization of the model. Yet finding a counterexample in the model directly is very often easier than finding a deductive proof in the logic. Some people got a Turing award for that discovery. > Doesn't mean we need to willfully embrace blind faith in incomplete induction. Formal methods is not "blind faith". Second, we haven't willfully given up on deductive proofs; it's just that for decades we've tried to scale them and couldn't, so out of necessity we found methods that have worked better in practice. I don't know if 200 years from now people won't be able to make deductive proofs feasible, but why not use formal methods to make our software better and cheaper now? In any event, all I want is for people to know (what formal methods research and practice already does) that software correctness is an extremely complex topic, with severe challenges that are both theoretical and practical, and anyone who suggests that there is a known specific solution to the problem or that one of the many imperfect avenues we're exploring is "the future", doesn't know what they're talking about.

permeakra 7y ago
>Sure, but let's say that it's a conservative estimate that 99% don't need proofs 99% don't need formal verification, they are OK with unit tests. If one is actually that concerned with an effort to perform actual verification, they most likely want an actual proof. >The logic is already a formalization of the model. So? >it's just that for decades we've tried to scale them and couldn't, For decades people didn't care for formal verification. Absolute majority of 'engineers' don't see any use in it. You, on the other hand, see little use for formal verification with dependent types. Well, forgive me for drawing a parallel here. I want some specific guarantees that are fairly easy to express and keep track with dependent types, not some fancy offshot of Hoare logic. Why would I care for a method clearly inferior for my use cases? == Let's return a bit and examine one specific case again. Consider situation: one writes a generic merge-join function over sorted arrays. There, input arrays must sorted with same predicate over same, possibly virtual, key. To express this in specification on the input data one need to - quantify over the types of both arrays - quantify over the type of the key - and all the functions able to produce a key of this type from elements of array 1 - and all the functions able to produce a key of this type from elements of array 2 - quantify over the ordering predicate over values of the key type - express that ordering holds for each pair of elements of the array -- i.e. quantify over indicies of arrays 1 and 2. - For which one needs information on index bonds attached to arrays I can, with some effort, express it in the language of type theory. I'm very interested how one can express it using, say, first order logic that, you know, doesn't allow for quantification over predicates.
- pron 7y ago
  > 99% don't need formal verification, they are OK with unit tests. Formal verification can be cheaper than tests. It's not just about a higher confidence, but also about achieving similar confidence more cheaply. That's one of the reasons why deductive proofs are not so popular in formal methods research -- they're too inflexible. > If one is actually that concerned with an effort to perform actual verification, they most likely want an actual proof. But we don't need to hypothesize -- they don't. Almost all formal verification in industry uses model checkers and sound static analysis. If you are interested in addressing the needs of certain small niches, that's one thing, but the thrust of formal methods research is about helping as much software as possible, and so deductive proofs are not the focus, because they're well behind other methods. > So? So, if you have a model checker, you don't need to write a proof. The model-checker could automatically provide a model-theoretical proof for you, at the press of a button. That's how, say, avionics software is verified. That's how Intel's chips are verified. People can't afford to write proofs for that volume of software. People write proofs only when model checking fails, or to tie together model checking results. It's no one's first choice (unless they're researchers or hobbyists). > For decades people didn't care for formal verification. It doesn't seem like you're familiar with the field. There was a huge boost in formal methods in the 70s followed by a research winter when people over promised and underdelivered. Then, about 20 years ago, there was a resurgence with different goals. In general, research now focuses on managing cost vs. benefit, reducing certain kinds of bugs, and finding ways to make verifiation more flexible, as we've so far been unable to make end-to-end verification scale. > Why would I care for a method clearly inferior for my use cases? I don't understand why you think it's inferior. It is absolutely not, and it is superior where it matters most. Expressiveness is the same, so specification is the same, but verification is flexible. You can use deductive proofs, or verifiation methods that have shown more promise. > I'm very interested how one can express it using, say, first order logic that, you know, doesn't allow for quantification over predicates. What? Of course FOL allows quantification over predicates and functions if they are elements of the domain, as they are in say, set theory (in fact, there is an assumption at the base of modern logic, that any mathematical theory could be expressed in some first-order language). Or, you could use HOL, if you like. But again, the theory is not the problem here. It's the chosen verification tool (and BTW, formal methods practitioners normally prefer to weaken the specification power if it reduces the cost of verification). Your example, in particular, is easily expressed in FO set theory, or many kinds of many-sorted FOL, or in HOL. For example, ∀ K, V . ∀ f ∈ K → V . ... is a trivial, perfectly normal, first-order logic over sets. In fact, dependent type theories like Lean's strive to be interpretable in set theory. But really, the choice theory is the least important issue with dependent types or software verification in general. If you are, however, interested in theory (as I am), you can read my series on TLA+. It is a first-order logic that is strictly richer and more expressive than lambda-calculus-based dependent type theories (unless you deeply embed it in them, and describe your computations in monads): https://pron.github.io/tlaplus https://pron.github.io/tlaplus