5 ms·

> Sure, that's how abstract interpretation works. But it doesn't always work, and proving termination says absolutely nothing about proving other properties. A

by fmap 10y ago

> Sure, that's how abstract interpretation works. But it doesn't always work, and proving termination says absolutely nothing about proving other properties. Abstract interpretation has nothing to do with disjunctive well-foundedness. The latter is a specific proof method which has pretty much revolutionized automated termination proving in the early 21st century (due to being modular and therefore allowing for easy combination of decision procedures). >> Does the consistency of ZFC "elude the power of math"? > Yes. Yet I can easily show ZFC consistent in CiC with excluded middle at Type. Sets are graphs modulo bisimilarity, choice follows from excluded middle at type. Conversely, classical CiC is consistent relative to ZFC with enough Grothendieck universes. Math doesn't end at ZFC, and no, not even in practice (higher category theory pretty much requires these constructions). > I'm not sure what you mean by "apart from it being too expensive". But it's like saying that there are no known fundamental restrictions that prevent us from proving P /= NP or the Goldbach conjecture, but stating confidently that either will be accomplished in some known timeframe is a whole other matter. One of them requires lots of perspiration, the other requires some fundamental new insight. This is not science fiction. It's not even fiction. You can sit down right now and show the correctness of arbitrary data structures and algorithms in Coq, using, e.g., Charguéraud's CFML. You can even verify arbitrary C programs, using VST, even though I wouldn't recommend it (seeing what guarantees the C semantics really give you, compared to your mental model of C can lead to night terror in adults).

pron 10y ago
> Abstract interpretation has nothing to do with disjunctive well-foundedness. Abstract interpretation has to do with every proof technique regarding computation. > The latter is a specific proof method which has pretty much revolutionized automated termination proving in the early 21st century (due to being modular and therefore allowing for easy combination of decision procedures). That's great, and model checking and abstract interpretation completely revolutionized many kinds of program proofs -- termination, temporal logic, memory safety and many more -- but the fact remains that no one has ever been able to fully verify a large real-world program using any known technique, and no one -- to the best of my knowledge -- seems to think we're on the path that will get us there any time soon. You'll find that the people who use formal methods on a regular basis (like me, if only in the past year or so) are the ones that are most cautious about pie-in-the-sky promises. Yes, some things will get easier; yes some properties will become easy to prove. But full, affordable program verification? Probably not in the foreseeable future, if ever. People like Xavier Leroy, who are experts in deductive verification methods are always very cautious about making such optimistic promises. Leroy, e.g. believes that deductive methods are suitable only for smallish programs. In fact, when it comes to manual formal verification, I am not aware of anyone who claims they will become generally affordable any time soon. Automated methods (model checkers and SMT solvers) are used almost exclusively for real-world programs, with only a small smattering of manual deduction, usually to tie together automated results. Right now, the goal for manual deduction is to match the cost of current high-assurance development (which is too expensive for ordinary programs, if possible at all, due to size). Manual deduction also seems especially sensitive to algorithm complexity (not computational complexity, but "conceptual" complexity, which may be related (perhaps to space complexity more than time complexity)), but really the potential effectiveness of various methods to affordable whole-program verification is no more than a personal affinity at this point. No one has anything definitive to claim. What I do find interesting is that it is PLT fans (maybe not the researchers themselves who are usually more cautious) who make the most outlandish claims despite the fact that when it comes to verification, PLT has had less real-world success than pretty much any other approach. Perhaps it's because those techniques are least put to the test, so there are no disappointments. > Yet I can easily show ZFC consistent in CiC with excluded middle at Type. I don't understand. Then the same result applies to CoC. There is nothing intrinsically special about ZFC as a formal foundation, it's just what most people take as the foundation. If you want to base math on another foundation go ahead, but an unprovable program exists in whatever foundation suits your taste, too. > One of them requires lots of perspiration, the other requires some fundamental new insight. You've just thrown all of complexity theory out the window. "Lots of perspiration" can mean (provably!) more resources than the entire universe can afford. Theoretically winning at Go also required little insight; actually winning required a lot of insight (namely, restricting the problem to facing human opponents and studying their behavior). If anything, it is the difference between decidability and undecidability that is of lesser importance than difference in "perspiration".
- fmap 10y ago
  > Abstract interpretation has to do with every proof technique regarding computation. Are we talking about the same thing? Abstract interpretation as formulated by Cousot consisting of a covariant galois connection between a particular kind of denotational semantics (collecting semantics) and a complete lattice with finite height or well-founded widening/narrowing functions. It's not the final word in program logics by a long shot. For example, collecting semantics is lossy for reactive systems and ... I'm not even sure what the story with concurrency is. I know that Cousot and others extended it to higher order languages at some point, but this is not mainstream as far as I know. > I don't understand. Then the same result applies to CiC. There is nothing intrinsically special about ZFC as a formal foundation, it's just what most people take as the foundation. Whichever foundation you choose, an unprovable program exists. Yes, and this is the true point of Goedel's proof and the (partial) failure of Hilbert's program. In this case you cannot have your pie and eat it too. You can't quote Hilbert to claim that ZFC is the accepted foundation of mathematics and then quote Goedel to say that this doesn't work. Goedel's results are not just making a statement about programs, they demonstrate the failure of mathematical realism, and even Goedel himself never quite got over it. > You've just thrown all of complexity theory out the window. "Lots of perspiration" can mean more resources than the universe can afford. I didn't even consider that you believed this to be the problem. The thing you have to understand is that there are not that many PLT researchers. The group around Xavier who are responsible for CompCert conists of a handful of people and most of the work was done in < 5 years. Most startups in SV are better funded and staffed than pretty much every formal verification project. CompCert with a single backend (there are 3 official backends, with several ABI targets each) has about 60 kloc of ML code when extracted and about 100 kloc more in Coq proofs, the factor between code and proof you are looking at is about 1:2. Most importantly, and unlike model checking or other completely automatic approaches, this is apparently a constant factor. So a good approximation is that you would have to write a program which is twice as large as the linux kernel (~20 mloc) plus the related tooling. This is certainly a big project, but I'm positive that we can meet your deadline of "before the heat death of the universe".
  - pron 10y ago
    > Abstract interpretation as formulated by Cousot consisting of ... Abstract interpretation is the general theory of Galois connections on program representations be they syntactic or abstract Kripke structures. Any sound abstraction (i.e. reduction) of the state space -- syntactic or semantic -- that preserves logical properties for the sake of verification is basically abstract interpretation. Widening/narrowing are just techniques to create sound reductions through fixpoints; I don't think they're essential to the concept of abstract interpretation (Cousot calls model checking, type systems and deductive proofs special cases of abstract interpretation). > You can't quote Hilbert to claim that ZFC is the accepted foundation of mathematics and then quote Goedel to say that this doesn't work. I didn't "claim" that ZFC is the accepted foundation. It is the normally assumed foundation so I picked it, but the choice is irrelevant. > Most startups in SV are better funded and staffed than pretty much every formal verification project. And need to build far bigger things. > this is apparently a constant factor. I would be extremely careful saying that. It is a constant factor when extreme care is taken to keep algorithms "braindead simple" (as someone who'd worked on seL4 once called it) and when the program size is kept to somewhere between tiny and small. > but I'm positive that we can meet your deadline of "before the heat death of the universe". Yes, obviously. The problem with all formal methods, though, is that the deadline isn't the end of the universe, but something that is considered affordable. My personal issue with manual deduction in general (I have more particular concerns with some PLT approaches) is that the approach is less amenable to approximate verification. In other words, making full-program end-to-end verification cheaper would not affect most software as it would still be too high a price (at least for the foreseeable future) to pay for something most software doesn't need. A bigger impact would be to reduce the cost of gaining the currently (or somewhat better) attainable level of confidence.

by fmap 10y ago

pron 10y ago

> Abstract interpretation has nothing to do with disjunctive well-foundedness. Abstract interpretation has to do with every proof technique regarding computation. > The latter is a specific proof method which has pretty much revolutionized automated termination proving in the early 21st century (due to being modular and therefore allowing for easy combination of decision procedures). That's great, and model checking and abstract interpretation completely revolutionized many kinds of program proofs -- termination, temporal logic, memory safety and many more -- but the fact remains that no one has ever been able to fully verify a large real-world program using any known technique, and no one -- to the best of my knowledge -- seems to think we're on the path that will get us there any time soon. You'll find that the people who use formal methods on a regular basis (like me, if only in the past year or so) are the ones that are most cautious about pie-in-the-sky promises. Yes, some things will get easier; yes some properties will become easy to prove. But full, affordable program verification? Probably not in the foreseeable future, if ever. People like Xavier Leroy, who are experts in deductive verification methods are always very cautious about making such optimistic promises. Leroy, e.g. believes that deductive methods are suitable only for smallish programs. In fact, when it comes to manual formal verification, I am not aware of anyone who claims they will become generally affordable any time soon. Automated methods (model checkers and SMT solvers) are used almost exclusively for real-world programs, with only a small smattering of manual deduction, usually to tie together automated results. Right now, the goal for manual deduction is to match the cost of current high-assurance development (which is too expensive for ordinary programs, if possible at all, due to size). Manual deduction also seems especially sensitive to algorithm complexity (not computational complexity, but "conceptual" complexity, which may be related (perhaps to space complexity more than time complexity)), but really the potential effectiveness of various methods to affordable whole-program verification is no more than a personal affinity at this point. No one has anything definitive to claim. What I do find interesting is that it is PLT fans (maybe not the researchers themselves who are usually more cautious) who make the most outlandish claims despite the fact that when it comes to verification, PLT has had less real-world success than pretty much any other approach. Perhaps it's because those techniques are least put to the test, so there are no disappointments. > Yet I can easily show ZFC consistent in CiC with excluded middle at Type. I don't understand. Then the same result applies to CoC. There is nothing intrinsically special about ZFC as a formal foundation, it's just what most people take as the foundation. If you want to base math on another foundation go ahead, but an unprovable program exists in whatever foundation suits your taste, too. > One of them requires lots of perspiration, the other requires some fundamental new insight. You've just thrown all of complexity theory out the window. "Lots of perspiration" can mean (provably!) more resources than the entire universe can afford. Theoretically winning at Go also required little insight; actually winning required a lot of insight (namely, restricting the problem to facing human opponents and studying their behavior). If anything, it is the difference between decidability and undecidability that is of lesser importance than difference in "perspiration".

fmap 10y ago
> Abstract interpretation has to do with every proof technique regarding computation. Are we talking about the same thing? Abstract interpretation as formulated by Cousot consisting of a covariant galois connection between a particular kind of denotational semantics (collecting semantics) and a complete lattice with finite height or well-founded widening/narrowing functions. It's not the final word in program logics by a long shot. For example, collecting semantics is lossy for reactive systems and ... I'm not even sure what the story with concurrency is. I know that Cousot and others extended it to higher order languages at some point, but this is not mainstream as far as I know. > I don't understand. Then the same result applies to CiC. There is nothing intrinsically special about ZFC as a formal foundation, it's just what most people take as the foundation. Whichever foundation you choose, an unprovable program exists. Yes, and this is the true point of Goedel's proof and the (partial) failure of Hilbert's program. In this case you cannot have your pie and eat it too. You can't quote Hilbert to claim that ZFC is the accepted foundation of mathematics and then quote Goedel to say that this doesn't work. Goedel's results are not just making a statement about programs, they demonstrate the failure of mathematical realism, and even Goedel himself never quite got over it. > You've just thrown all of complexity theory out the window. "Lots of perspiration" can mean more resources than the universe can afford. I didn't even consider that you believed this to be the problem. The thing you have to understand is that there are not that many PLT researchers. The group around Xavier who are responsible for CompCert conists of a handful of people and most of the work was done in < 5 years. Most startups in SV are better funded and staffed than pretty much every formal verification project. CompCert with a single backend (there are 3 official backends, with several ABI targets each) has about 60 kloc of ML code when extracted and about 100 kloc more in Coq proofs, the factor between code and proof you are looking at is about 1:2. Most importantly, and unlike model checking or other completely automatic approaches, this is apparently a constant factor. So a good approximation is that you would have to write a program which is twice as large as the linux kernel (~20 mloc) plus the related tooling. This is certainly a big project, but I'm positive that we can meet your deadline of "before the heat death of the universe".
- pron 10y ago
  > Abstract interpretation as formulated by Cousot consisting of ... Abstract interpretation is the general theory of Galois connections on program representations be they syntactic or abstract Kripke structures. Any sound abstraction (i.e. reduction) of the state space -- syntactic or semantic -- that preserves logical properties for the sake of verification is basically abstract interpretation. Widening/narrowing are just techniques to create sound reductions through fixpoints; I don't think they're essential to the concept of abstract interpretation (Cousot calls model checking, type systems and deductive proofs special cases of abstract interpretation). > You can't quote Hilbert to claim that ZFC is the accepted foundation of mathematics and then quote Goedel to say that this doesn't work. I didn't "claim" that ZFC is the accepted foundation. It is the normally assumed foundation so I picked it, but the choice is irrelevant. > Most startups in SV are better funded and staffed than pretty much every formal verification project. And need to build far bigger things. > this is apparently a constant factor. I would be extremely careful saying that. It is a constant factor when extreme care is taken to keep algorithms "braindead simple" (as someone who'd worked on seL4 once called it) and when the program size is kept to somewhere between tiny and small. > but I'm positive that we can meet your deadline of "before the heat death of the universe". Yes, obviously. The problem with all formal methods, though, is that the deadline isn't the end of the universe, but something that is considered affordable. My personal issue with manual deduction in general (I have more particular concerns with some PLT approaches) is that the approach is less amenable to approximate verification. In other words, making full-program end-to-end verification cheaper would not affect most software as it would still be too high a price (at least for the foreseeable future) to pay for something most software doesn't need. A bigger impact would be to reduce the cost of gaining the currently (or somewhat better) attainable level of confidence.