It doesn't appear that we're disagreeing. You're referring to verifying 'lots' of safety properties, I referred to verifying that an algorithm does everything

It doesn't appear that we're disagreeing. You're referring to verifying 'lots' of safety properties, I referred to verifying that an algorithm does everything it's supposed to. These are not the same thing in the general case. My actual point was that generic incompleteness and undecidability theorems do not guarantee that any given program must be defective. The thrust of langsec is in fact to parse all inputs at the boundaries, using algorithms with known properties, that is, ones where it's feasible to prove that they'll halt, won't overrun buffers, and so on.