[Ono-Sendai]

My functional language Winter has errors like that. You can compute the maximum memory usage of the program and then throw an error if it exceeds some threshold.

Edit: I'll add that there are lots of programs the prover can't effectively handle right now, so can't compute a good memory bound. It works fine for some relatively simple programs however.

[MaxBarraclough]

> there are lots of programs the prover can't effectively handle right now

And always will be, due to Rice's Theorem. Can still be useful though - various formal methods techniques are like this.

[Ono-Sendai]

Winter is not a Turing equivalent language, so technically Rice's theorem doesn't apply (I think). Nevertheless practically speaking you are right, there will always be valid programs that the prover can't prove are correct.