3 ms·

Another thing that prevents dependently-typed languages from being the future is that there are alternative verification methods that have so far shown greater

by pron 7y ago

Another thing that prevents dependently-typed languages from being the future is that there are alternative verification methods that have so far shown greater promise (and receive even more grants). I think the reason for this is that some hear of those languages because they're fans of programming languages in general and maybe know something about programming language theory, and dependent types represent this discipline in formal methods research. But if you look at formal methods research more generally (e.g. read the programs of the relevant conferences), you see that this direction of dependent type systems is relatively small, and most of the research effort is focused elsewhere. I feel that some of the discussion about those languages is like an amateur runner who's thoroughly amazed by the results of an Olympic runner to the point of obsession, without knowing that they're in the seventh place. So dependently typed languages have had some achievement, but other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. The main challenge, which you alluded to, is one of scale. So far only very small programs have been verified using any semi-manual formal deductive proof methods (of which dependent type systems are one instance), and other methods have shown somewhat better scalability.

zozbot234 7y ago
> other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. These techniques are tailored towards efficiently finding refutations or counterexamples where a program fails correctness. They are very effective at what they do, but they're best used in combination with formal proof, or as a sort of glorified automated testing ('fuzzing').
- pron 7y ago
  First, model checking is a proof technique, albeit in the model theory of the logic rather than in the proof theory; that it can find refutations is a major strength, though. Second, engineers build systems, and they care about the correctness of their system. This is something that cannot possibly be proven because a system is a physical object, and at best, what you can get are probabilistic guarantees (e.g. the CPU only performs the commands it is given with some probability). So what engineers want (as opposed to mathematicians or computer scientists publishing an algorithm) is a technique that most cheaply brings their system to the required correctness probability. Whether this means proving the algorithm correct or finding as many bugs as possible is completely irrelevant. So far, automated techniques like the ones I mentioned do a better job at that, and that is why they're currently considered more promising.
  - zozbot234 7y ago
    > First, model checking is a proof technique It is a proof technique if you're exhaustively checking a finite model, but the usual meaning of "model checking" is not restricted to that case. You may be right that just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. Probably for "global", cross-cutting properties where formal proof might be expected to be difficult.
    - pron 7y ago
      > but the usual meaning of "model checking" is not restricted to that case It is. That's the definition of the term "model checking" ("model" means a satisfying assignment for a logic formula). Some model checkers (like CEGAR) also exhaustively check infinite-state specifications (although, obviously, not in every case; BTW, that model checkers are exhaustive, meaning sound, does not mean that they operate by brute-force -- they do not). You are, however, correct that sometimes we model check only a finite instance of a program/spec with infinite states, but in this case it is that restricted spec that is model-checked. That is one of the many ways in which model checking is more flexible than deductive proofs. > just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. It would, does, and must suffice for all use cases, and besides, there is no other alternative. > Probably for "global", cross-cutting properties where formal proof might be expected to be difficult. No real system can be guaranteed to be correct. It is a physical impossibility. There is simply no such thing as a system that is "proven correct" in formal methods; the best you can hope for is an algorithm that is proven correct or a system that is correct with probability. Even exhaustive (i.e. sound) techniques like formal deductive proofs and model checking only guarantee the correctness of a system with probability. An algorithm that is proven to give the right answer is only a probabilistic guarantee that the system will (because the guarantee that the computer will execute the commands given to it correctly is only probabilistic). Mathematicians and algorithm authors can prove theorems; engineers only need, and can only ever hope for, probabilities. This is why while there may be some overlap in the computer-assisted techniques offered to mathematicians and algorithms writers, the study of software verification is concerned with a different problem.

by pron 7y ago

zozbot234 7y ago

> other techniques -- from CEGAR model checking to concolic testing -- have had better results, and that's why they're getting more attention in the formal methods space. These techniques are tailored towards efficiently finding refutations or counterexamples where a program fails correctness. They are very effective at what they do, but they're best used in combination with formal proof, or as a sort of glorified automated testing ('fuzzing').

pron 7y ago
First, model checking is a proof technique, albeit in the model theory of the logic rather than in the proof theory; that it can find refutations is a major strength, though. Second, engineers build systems, and they care about the correctness of their system. This is something that cannot possibly be proven because a system is a physical object, and at best, what you can get are probabilistic guarantees (e.g. the CPU only performs the commands it is given with some probability). So what engineers want (as opposed to mathematicians or computer scientists publishing an algorithm) is a technique that most cheaply brings their system to the required correctness probability. Whether this means proving the algorithm correct or finding as many bugs as possible is completely irrelevant. So far, automated techniques like the ones I mentioned do a better job at that, and that is why they're currently considered more promising.
- zozbot234 7y ago
  > First, model checking is a proof technique It is a proof technique if you're exhaustively checking a finite model, but the usual meaning of "model checking" is not restricted to that case. You may be right that just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. Probably for "global", cross-cutting properties where formal proof might be expected to be difficult.
  - pron 7y ago
    > but the usual meaning of "model checking" is not restricted to that case It is. That's the definition of the term "model checking" ("model" means a satisfying assignment for a logic formula). Some model checkers (like CEGAR) also exhaustively check infinite-state specifications (although, obviously, not in every case; BTW, that model checkers are exhaustive, meaning sound, does not mean that they operate by brute-force -- they do not). You are, however, correct that sometimes we model check only a finite instance of a program/spec with infinite states, but in this case it is that restricted spec that is model-checked. That is one of the many ways in which model checking is more flexible than deductive proofs. > just getting the "probability" of some software failing to meet its spec low enough could suffice for some use cases. It would, does, and must suffice for all use cases, and besides, there is no other alternative. > Probably for "global", cross-cutting properties where formal proof might be expected to be difficult. No real system can be guaranteed to be correct. It is a physical impossibility. There is simply no such thing as a system that is "proven correct" in formal methods; the best you can hope for is an algorithm that is proven correct or a system that is correct with probability. Even exhaustive (i.e. sound) techniques like formal deductive proofs and model checking only guarantee the correctness of a system with probability. An algorithm that is proven to give the right answer is only a probabilistic guarantee that the system will (because the guarantee that the computer will execute the commands given to it correctly is only probabilistic). Mathematicians and algorithm authors can prove theorems; engineers only need, and can only ever hope for, probabilities. This is why while there may be some overlap in the computer-assisted techniques offered to mathematicians and algorithms writers, the study of software verification is concerned with a different problem.