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