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.

I just don't think we need turing completeness to solve the problems we try to solve with software. You bring up how humans can reason and prove correctness for our programs, but I say we just force them to do that (making our programs no longer turing complete). I don't think I've ever encountered a problem that required steps that I didn't think I would be able to prove halted.

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.”

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.