3 ms·

This technically correct comment would be actually useful, if it linked a fully automated prover, that is capable of proving any property of a program that fits

• wolfgke 7y ago
  > If you remove infinite tape, you go from undecidable to "just" exponentially complex. Which is a huge leap - we got from "impossible" to "possible in principle" and we now can do research how to make it even "sufficiently fast" for problems of practical relevance.
  • h91wka 7y ago
    No. In CIC I can prove that, say, some property is valid for _any_ natural number. Your "memory is bounded" argument is invalid, as formal proofs can go beyond that.