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