> What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof?

A formal proof is one that can be mechanically translated to the logic's deduction rules. An informal proof is anything that is considered by mathematicians as proof, yet isn't a formal proof. It is smaller because it skips many details, but seems convincing enough.

> it sounds as if you are ignoring all the progress we have made in programming language design

We have not made significant progress when it comes to proving global logical properties, and I don't think anyone claims we have. There are languages that in theory can be used to prove correctness; in practice they have never been successfully used on real world programs, except for small and simplified ones, and even then with great effort by experts.

> For example, C programs typically have a lot of bugs because...

The reason why many languages are safer than C is because they prevent certain bugs by enforcing local properties, like memory safety. This is an example of a local property (that's easy to prove, even automatically, in many cases) that is known to be the cause of many costly bugs. Other languages don't fare significantly better when it comes to proving global correctness. The best we've done -- and that's not insignificant -- is reduce accidental complexity to proof.

Like I show in my post, even a language with nothing but boolean variables and pure functions -- no memory allocation, no recursion or iteration of any kind and no higher-order functions -- where all programs are obviously terminating and the language is too weak to do anything useful, cannot be feasibly verified in general. Languages can help with local properties. The difficulty of proving logical correctness is dependent almost entirely on one thing: how simple your algorithm is.

> The "simple" imperative programming models that are still used almost everywhere have exactly the same problem.

So far imperative languages seem fare better than FP in terms of verification. Fully verifiable languages that are used for safety-critical realtime systems, are also imperative (although not in the same way JavaScript is).

Make sure that by reading papers in PLT you're not falling into a bias trap. PLT nowadays is mostly concerned with FP, so papers will be on FP. Those who are interested in the verification aspects of PLT, will write about ideas that they think show promise. But most of verification research isn't PLT, and deals with imperative (or language-agnostic) algorithms, and they have their own results, which are no less promising. Neither has been able to "solve" verification in the sense people hoped in the 70s, and AFAIK, neither community is trying to do that. That doesn't stop them from publishing results that are very promising, but haven't been proven in practice yet. But if you're exposed to only one community, you may get the false sense that there is one consensus approach (there isn't), and we're slowly but surely getting to our destination (maybe we are, but we don't know for sure, and we don't know which approach works in practice).

> for modular correctness proofs

The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. Certain properties which could prevent certain bugs can definitely be made easier to prove with modularity -- they're local in some way -- but certainly not global logical correctness. Some people may hope that global correctness would turn out to be decomposable in enough use cases, but this is an empirical conjecture, with little proof so far.

> Essentially, you have just taken part of the state space and shrunk it down to a single bit.

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 challenge is to figure out which properties that can prevent expensive bugs can be proved.

> So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions.

Theorems proven in math are much deeper yet deal with far simpler concepts than computer programs. The whole idea of computer programs is that they create small structures that defeat mathematical reasoning. It is no accident that Hilbert's program was laid to rest by the "discovery" of computer programs. Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely. The best analogy is physics. The gravity equation is simple, modular, pure, equational, algebraic, composable -- whatever good PL adjective you may hope to assign. It is so simple that it is completely uninteresting to mathematicians. Yet, combine two of those equations together -- they compose very nicely -- and already no closed-form solution exists and the behavior can no longer be predicted; it is uninteresting to mathematicians (well, except for some instances), but for the opposite reasons. Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem.

> We are making real progress in verification.

Absolutely, but the goals are different. Most of the time we're talking local properties or a lot of effort or restricted domains. 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.

BTW, most progress in verification is not in PLT. Restricting yourself to PLT is a sure way to miss most of it.