Re:The SeL4 Foundation: What and Why
by wolfgke on Tuesday April 07, 2020 @08:52AM
(#22802692)
> 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.
Re:The SeL4 Foundation: What and Why
by h91wka on Tuesday April 07, 2020 @08:58AM
(#22802743)
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.
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.