Your "correcting" by asserting I'm wrong and then saying absolutely nothing to contradict it is perhaps the style of correctness you're familiar with, and if you've made that into a small career, than all I can say is that I'm sorry.

The fact that some programs can be verified, regardless of means or formalism (why do you think the formalism matters is beyond me, but is in line with your general name-dropping that is backed by little actual erudition) does in no way contradict the theorem that you cannot decompose correctness generally. Moreover, I don't know how you tout the immense cost in practice of achieving moderate levels of success as some sort of practical counteraxample. The best we've done so far is years of work by world experts leading to end-to-end verification of programs the size of 1/5 of jQuery. It's like you're jumping up and down showing a successful transmutation of five lead atoms into gold atoms in a one-billion-dollar particle accelerator as counterevidence of the claim that transmuation is not yet practically infeasible.

To put it simply, can you point out what exactly in the links and claims you've listed contradicts even a single thing of what I've said? Why do you insist on berating me while vigorously agreeing?