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.