I just want to point out that you don't need to know the precise bounds of such a computational model to prove things about your programs. There already exist Turing-complete programming languages where you can prove non-trivial properties about your program and which have had practical applications, for example F* and its use in Project Everest.
Just having a language that allows you to prove things does not mean it is possible to prove them.
We still don't know if it is possible to build a provably correct multi-tasking OS or a web browser without security vulnerabilities. If it was easy we would already have one written in FStar or Idris.
While admiring all the work done by Project Everest - the fact is that it is a
multi-year project (I first read about it about 3-4 years ago and it was already under way) with a very limited scope - it is more of an evidence of difficulties of writing correct software.
https://project-everest.github.io/
https://www.fstar-lang.org/