|
|
|
|
|
|
by Ono-Sendai
2226 days ago
|
|
|
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. |
|
|