> 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). 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.
> 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.
I have no idea what you just said, but I believe you :)
> it depends on your abstractions being connected to the same kind of semantics.
I'm side-tracking, but "semantics" requires a language. Not all computations are expressed in a language, and AI applies even to those of them that are not.
> If there was an interesting problem which was provably independent of ZFC, people wouldn't just give up.
Again, this is not the point. Whatever logic you choose, there would be programs whose behavior you cannot predict.
> You don't have to look to programs to find questions which are apparently "beyond math".
Of course, but we're talking about programs, and no one can deny the role of programs in the history of mathematics as examples of things that are hard (or impossible) to reason about.
> 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.
This is indeed the main point of debate, although I'm not insisting on "exponential". The theory says things can in be really expensive (exponential and more), and the question is whether real-world programs are contained in a subset that is entirely different -- easy to verify -- or that they are spread throughout and can turn out to be arbitrarily hard (close to the worst case). I don't think empirical evidence settles this question, and it certainly doesn't suggest real programs are easy to verify. It is also certainly true that some programs -- when kept small and very simple -- in some specific domains, under lab conditions, have turned out to be not so terrible to verify. As someone who practices formal methods almost every day, I will certainly not say that things are hopeless, but I don't think we're in a position to say that the solution is near. We really don't know enough.
As someone who uses formal methods to reason about very complex distributed and concurrent algorithms (although deductive proof would take far more resources and time than we can hope to spend), formal verification works well (although I and many others who do this in the industry are skeptical about deduction), but the problem is different from program verification.
> This seems like a sweet spot for most applications.
Oh, I have no argument with you there. I totally agree. Deductive methods for the small, sensitive core if automated methods don't work, and automated methods -- with various degrees of confidence -- for the rest. But this isn't the same as saying that PLT approaches have "solved verification".
> This is why I focus so much on program logics and PLT methods.
Have you given TLA+ a look? I think it covers exactly what you're looking for far better than any PLT solution I've ever seen, for many reasons (generality, simplicity, ease, tooling, elegance). I'm always amused when I see yet another academic paper about formulating something in Coq, that an "ordinary" engineer would do with no more than little thought within a month of first laying eyes on TLA+. Just today I watched this talk from ICFP: https://www.youtube.com/watch?v=caSOTjr1z18 It didn't really make me understand what HoTT is about, but it did make me realize that PLT has taken a wrong turn somewhere and seems to be falling into the rabbit hole of foundational logic, if so much thought is put into a "computation" that isn't even algorithmic (i.e., it has a computational complexity of 0, and serves not the program but the formalism). If I remember correctly, "older" typed languages that PLT people are fond of like SML, didn't even have this problem that now requires a new foundation for mathematics (I'm exaggerating, but I think that not by much).
------
This, BTW, is a Twitter conversation between PLT-verification people, one of whom has worked on seL4. The bottom line is that we should work on FM -- it works in many cases -- but certainly "dismiss illusions" about it:
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). 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.