4 ms·
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 threshol
by Ono-Sendai 6y ago
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 6y 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 6y 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.