3 ms·
> 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 form
by MaxBarraclough 7y ago
> 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 7y agoWinter 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.