The halting problem is a product of a Turing-complete model of computation.
If we want perfectly secure systems, then perhaps we don’t want universal and general purpose ones.
The bar for Turing-complete is very low. The halting problem is to programming as Godel's incompleteness theorem is to metamathematics. Yet no one is seriously suggesting that we downgrade to axiomatic systems incapable of expressing Peano arithmetic, nor that our current axiomatic systems are impractical for proving theorems.
We cannot automatically and completely verify nontrivial semantic properties of arbitrary programs written in a Turing-complete language (Rice's theorem), but as long as we as humans can intuit correctness arguments for our programs, then formal methods will apply to it. Of course, declarative rather than imperative programming semantics tend to result in simpler correctness arguments, sidestepping reliance on global state and convoluted loop invariants.
And maybe we discover that perfectly secure systems are not useful, or fun, or otherwise enjoyable to use.
Maybe the digital equivalent of being locked in a doomsday bunker eating only white rice doesn't produce interesting software experiences.
One can imagine a world in which Rust allows a `decidable` block and code has stricter guarantees within it.
I imagine it would be a nightmare to work with.
Software “engineers” aren’t responsible for their code the same way professional engineers are. Yet, I’d prefer the embedded system for the supermarket freezer were a nightmare to work with, over a society that is a nightmare to live in because of “cyber.”