I hope readers will be able to look past this one sentence in your post and take a good hard look at the rest of it, which is quite important.
In real conditions, static analysis and theorem proving can verify lots of safety properties. See e.g. Astrée & Airbus, or F* and Project Everest.
IMHO, the solution is to use static analysis in conjunction with DSLs that have restricted semantics to make static analysis and hand-written proofs easy.
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.
> If these folks can make safe parsers for PDF (https://www.darpa.mil/program/safe-documents) it should be possible for anything
It is, but it's very expensive. That's why a lot of this research has been getting billions in funding for 10-15 years now in order to build out the underlying ecosystem needed to harden the entire stack
There is a "problem of political will" but also the problem of stupid SW which tries very high to decode everything you throw at it. Some time ago it was "file format not recognized", nowadays it is a root exploit.
Specifically, we're using context-sensitive and Turing-complete parsers up and down the software stack, which (at the Turing-complete level of complexity, says Gödel) guarantees that determined attackers can expect to discover an exploitable "weird machine."
Folks should watch this panel and other talks by Meredith L. Patterson (co-collaborator and wife of the late Len Sassaman) and Sergey Bratus (previously at DARPA, now Dartmouth) to get a sense of the problem and the solution.
https://youtu.be/8tAxHrntBJs?t=806
These folks are saying that, just as the industry handled over-the-wire insecurity with TLS and e2ee (and not rolling our own crypto) we can handle device exploitability with well-described data and automated parser generation from those descriptions (and not rolling our own parsers, which these folks say should be verboten for the same reason as rolling one's own crypto: parsing is too hard for non-specialists to get right).
Moreover, we don't have to redo the whole stack for it to be meaningful: big players can start using this tooling (e.g. https://github.com/UpstandingHackers/hammer) for parsers handling data from very untrustworthy inputs, such as message payloads sent to a phone number.
Apple's Lockdown mode is a step in this direction, though in such a crude, "burn the village" way that it makes the phone almost unusable. But sacrificing usability shouldn't be necessary with current methods. If these folks can make safe parsers for PDF (https://www.darpa.mil/program/safe-documents) it should be possible for anything.
Another great talk: https://www.youtube.com/watch?v=3kEfedtQVOY