> 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.