> The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be.

You are seriously overselling these results. Here's one way to make termination proofs modular: Take the graph of your function (vertices for each value of the arguments, edges for recursive calls) and take its transitive closure. If you can cover the transitive closure with an arbitrary number of individually well-founded relations, the function terminates.

> Yes, this is what abstract interpretation does, and types carry it out. But not every property survives this state reduction (most of them don't).

The point of having contextual equivalence or a program logic is that every property you can express in your programming language/logic survives this state reduction.

> Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely.

You give an example of a termination problem which is equivalent to the consistency of ZFC. Does the consistency of ZFC "elude the power of math"? It's certainly a very simple question, much easier to write down than the Turing machine in question.

> Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem.

This applies to mathematics as well. You can write down simple sounding questions, like the Collatz conjecture you mention, which are actually extremely complicated. This is the point where complexity theory comes into the picture. For instance, I could generate random types in the calculus of constructions (random propositions) and ask if that type is inhabited (the proposition is provable). This is an undecidable problem and for complexity theoretic reason most instances (of a certain shape) will actually be hard.

The concepts in programming aren't inherently more complicated than the concepts in mathematics. If anything, there are plenty of natural concepts in mathematics which behave far more chaotically than anything in CS (look at a table of homotopy groups of spheres and tell me where that pattern comes from).

> Most of the things you mention that are relevant to global properties have so far failed to scale to real-world programs. Affordable proof of ordinary software's global correctness is no longer a goal and certainly not a promise of contemporary software verification.

It's very much the goal for PLT. :)

In practice, it's also very much in the future. Right now verifying large programs is possible for a team of experts with a lot of time and money. A lot of the work in the 21st century has been to scale these theoretical methods to real languages. Most of the really big verification projects of today were unthinkable a decade ago. A decade or two in the future it'll probably be routine and just another tool you use, similar to static analysis or unit tests.

Right now the infrarstructure is just not there yet, and that's one of the reasons why formal verification is so expensive. But there are no fundamental restrictions which would prevent us from verifying, say, the Linux kernel. Apart from it being way too expensive. If it was written in a reasonable languages, which encouraged programmers to develop truly sound abstractions it could be orders of magnitude less expensive, though...