6 ms·

> Abstract interpretation has to do with every proof technique regarding computation. Are we talking about the same thing? Abstract interpretation as formulate

by 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.
- fmap 10y ago
  > Cousot calls model checking, type systems and deductive proofs special cases of abstract interpretation Maybe he said something like "[...] can all be seen as abstract interpretations". But it's probably not always useful to do so. Abstract interpretation has been enormously successful, not least because it is modular: there are standard ways of combining abstract domains. This is a huge advantage, especially compared to ad-hoc techniques in program verification, but it depends on your abstractions being connected to the same kind of semantics. In particular, disjunctive termination proofs can be shown to be sound through Ramsey's theorem, and I don't see how to formulate this as an adjunction at all. Even if it is theoretically possible, the statement is a bit like saying that "all programming languages are equivalent to Turing machines". Even if that is true in principle, you wouldn't want to develop your next product as a big string rewriting system... > I didn't "claim" that ZFC is the accepted foundation. The point is, that these questions are not "beyond the power of math". Mathematics is like an amorphous blob, which expands as needed to encompass new and interesting problems. If there was an interesting problem which was provably independent of ZFC, people wouldn't just give up. They would try to look for "natural" or "intuitive" extensions in which the problem can be "settled". Case in point, the continuum hypothesis is independent of ZFC, and so people developed extensions where the answer could be settled either way. Goedel himself was convinced that this is a question which could be "answered" by identifying which of the proposed extensions is more "natural". You don't have to look to programs to find questions which are apparently "beyond math". Any kind of self-referential statement gives you such a question. Programs are not special in this regard, you could always do the same thing in logic. > 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. This is mostly a question of economics. In research, you have tight time constraints and comparatively little man power. You can take current data structures for weak memory concurrency and verify them end to end, but if the goal of your project is "building a verified C compiler", then this is not a good use of your time. In truth, big research projects are just as conservative as big companies, if not more so. The architecture of CompCert (as originally implemented) is at a level you would find in an 80s handbook on compiler construction. This is not because Xavier doesn't know better (see OCaml), it's because they absolutely couldn't afford for the project to fail, or even to be delayed. In my experience, complex data structures and algorithms aren't actually that much more complicated to verify than simple ones. The main work is always in finding the right specifications, and modelling the problem in your proof assistant. For instance, if you have to verify a max-flow solver, then you will need to formalize graphs, flows on graphs, and duality. This is for writing down the specification (what is a maximum flow) and showing that it has the right properties (e.g., is unique). Once you have all of this machinery, the final correctness proof of, say, the Edmonds-Karp algorithm is not a lot of work (see https://www21.in.tum.de/~lammich/pub/itp2016_edka.pdf https://www21.in.tum.de/~lammich/pub/itp2016_edka.pdf). Based on this background theory, it would also not be particularly difficult to verify some variant of Preflow-Push. But again, if you have a concrete problem you want to solve through max-flow, then you would be done once you have verified the abstract augmenting paths algorithm. Heck, in this case you would probably just verify a validator and implement the solver in untrusted (but memory safe) code. You know, seL4 is actually a good example of economic pressure on research projects. I don't know how to say this nicely, but the correctness proofs of seL4 are extremely ugly. There just wasn't enough time to look for elegant specifications or proofs, or to reformulate algorithms and data structures to make the proofs nicer. That's not to say that it cannot be done. It's certainly one goal of the CertiKOS project to build better tools for OS verification. > Yes, obviously. The problem with all formal methods, though, is that the deadline isn't the end of the universe Look, your argument was that the state space is exponential in the program size, therefore verification takes exponential time since it is fundamentally impossible to build modular correctness proofs. All I'm saying is that based on the empirical evidence, this is false. There are plenty of modular proof techniques and all formal verification projects (in the ITP sector) that I'm aware of report the overhead of verification as a constant factor. > 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. I completely agree with you on the last part, but what makes you think that we can't drop down the level of assurance for parts of the program? Chlipala's Bedrock project built a verified web server in Coq. The lowest levels of this (the implementation of threading, data structures, memory allocation, tcp stack, etc) verify full functional correctness, while for the higher levels (user interface, etc), they merely show the absense of run time errors. This seems like a sweet spot for most applications. You can verify full functional correctness for library code, or core OS components, while applications are merely free of memory errors or other bugs which could crash your program. How much money would you save in the long run if you knew for certain that the infrarstructure that is running your software cannot break? --- Personally, I think that the most promising application in the near future is actually just better documentation. If people were more aware of formal methods and would specify precisely what a certain function ought to do, we would probably eliminate a lot of bugs right there. I'd also expect that thinking more deeply about your programs should lead to better architectural decisions and better abstractions. But this doesn't work if you force people to use first-order logic, with some limited set of temporal operators. You need a language which is at least as expressive as the natural language specifications that people are already using. This is why I focus so much on program logics and PLT methods.

by fmap 10y ago

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.

fmap 10y ago
> Cousot calls model checking, type systems and deductive proofs special cases of abstract interpretation Maybe he said something like "[...] can all be seen as abstract interpretations". But it's probably not always useful to do so. Abstract interpretation has been enormously successful, not least because it is modular: there are standard ways of combining abstract domains. This is a huge advantage, especially compared to ad-hoc techniques in program verification, but it depends on your abstractions being connected to the same kind of semantics. In particular, disjunctive termination proofs can be shown to be sound through Ramsey's theorem, and I don't see how to formulate this as an adjunction at all. Even if it is theoretically possible, the statement is a bit like saying that "all programming languages are equivalent to Turing machines". Even if that is true in principle, you wouldn't want to develop your next product as a big string rewriting system... > I didn't "claim" that ZFC is the accepted foundation. The point is, that these questions are not "beyond the power of math". Mathematics is like an amorphous blob, which expands as needed to encompass new and interesting problems. If there was an interesting problem which was provably independent of ZFC, people wouldn't just give up. They would try to look for "natural" or "intuitive" extensions in which the problem can be "settled". Case in point, the continuum hypothesis is independent of ZFC, and so people developed extensions where the answer could be settled either way. Goedel himself was convinced that this is a question which could be "answered" by identifying which of the proposed extensions is more "natural". You don't have to look to programs to find questions which are apparently "beyond math". Any kind of self-referential statement gives you such a question. Programs are not special in this regard, you could always do the same thing in logic. > 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. This is mostly a question of economics. In research, you have tight time constraints and comparatively little man power. You can take current data structures for weak memory concurrency and verify them end to end, but if the goal of your project is "building a verified C compiler", then this is not a good use of your time. In truth, big research projects are just as conservative as big companies, if not more so. The architecture of CompCert (as originally implemented) is at a level you would find in an 80s handbook on compiler construction. This is not because Xavier doesn't know better (see OCaml), it's because they absolutely couldn't afford for the project to fail, or even to be delayed. In my experience, complex data structures and algorithms aren't actually that much more complicated to verify than simple ones. The main work is always in finding the right specifications, and modelling the problem in your proof assistant. For instance, if you have to verify a max-flow solver, then you will need to formalize graphs, flows on graphs, and duality. This is for writing down the specification (what is a maximum flow) and showing that it has the right properties (e.g., is unique). Once you have all of this machinery, the final correctness proof of, say, the Edmonds-Karp algorithm is not a lot of work (see https://www21.in.tum.de/~lammich/pub/itp2016_edka.pdf https://www21.in.tum.de/~lammich/pub/itp2016_edka.pdf). Based on this background theory, it would also not be particularly difficult to verify some variant of Preflow-Push. But again, if you have a concrete problem you want to solve through max-flow, then you would be done once you have verified the abstract augmenting paths algorithm. Heck, in this case you would probably just verify a validator and implement the solver in untrusted (but memory safe) code. You know, seL4 is actually a good example of economic pressure on research projects. I don't know how to say this nicely, but the correctness proofs of seL4 are extremely ugly. There just wasn't enough time to look for elegant specifications or proofs, or to reformulate algorithms and data structures to make the proofs nicer. That's not to say that it cannot be done. It's certainly one goal of the CertiKOS project to build better tools for OS verification. > Yes, obviously. The problem with all formal methods, though, is that the deadline isn't the end of the universe Look, your argument was that the state space is exponential in the program size, therefore verification takes exponential time since it is fundamentally impossible to build modular correctness proofs. All I'm saying is that based on the empirical evidence, this is false. There are plenty of modular proof techniques and all formal verification projects (in the ITP sector) that I'm aware of report the overhead of verification as a constant factor. > 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. I completely agree with you on the last part, but what makes you think that we can't drop down the level of assurance for parts of the program? Chlipala's Bedrock project built a verified web server in Coq. The lowest levels of this (the implementation of threading, data structures, memory allocation, tcp stack, etc) verify full functional correctness, while for the higher levels (user interface, etc), they merely show the absense of run time errors. This seems like a sweet spot for most applications. You can verify full functional correctness for library code, or core OS components, while applications are merely free of memory errors or other bugs which could crash your program. How much money would you save in the long run if you knew for certain that the infrarstructure that is running your software cannot break? --- Personally, I think that the most promising application in the near future is actually just better documentation. If people were more aware of formal methods and would specify precisely what a certain function ought to do, we would probably eliminate a lot of bugs right there. I'd also expect that thinking more deeply about your programs should lead to better architectural decisions and better abstractions. But this doesn't work if you force people to use first-order logic, with some limited set of temporal operators. You need a language which is at least as expressive as the natural language specifications that people are already using. This is why I focus so much on program logics and PLT methods.