Sure, but how many of those C programs are inherently hard to verify vs how many of them are hard because they happen to be built with tools that make them hard to verify?
I don't think those are fully separable concepts in legacy, spaghetti code.
Regardless, I agree that if you're willing to architect your system around the need to formally verify it, the problem is somewhat tractable and getting more so every year as tools improve. Non-experts still might need the occasional "justifiable shortcut" instead of proving everything, but it's doable.
Sure, I don't think anyone is realistically expecting to verify all existing legacy spaghetti code -- _that's_ an interesting research direction, at best.
The point upthread (at least the point I took) is not that existing code doesn't do things to make it difficult to verify, but rather there's no reason inherent to the desired behavior of those programs that it _needs_ to be difficult to verify them. Nor is there good reason going forward to not lean towards tools that make verification more tractable for anything new we write.
