halting problem not the issue

The problem is, though, that the state of the art is such that the only stuff you can prove secure (or haltable) is sufficiently trivial that the compiler could compute most of it itself and just tag this function KNOWN_SECURE or something. It's often easy to prove single functions secure in isolation. It's as soon as you start chaining them together (especially when conditionals, loops, and function calls interact) that the thing becomes hideous. This is doubly so if the function calls manipulate global state.

Now, let's be honest here. How many programs do you know that are pure filters? How many of these eschew conditionals, loops, and function calls, allowing analysis without horrible exponential explosions that have to be cut down with heuristic axes (losing proof power)?

(It is true that a lot of security-exposed stuff, like libpng, seems like a filter of sorts... only, oops, you forgot the memory allocator! Now almost nothing outside certain simple embedded applications is a filter. Even 'cat' is not.)