News for hackers. Stuff that matters.

A comment on The SeL4 Foundation: What and Why. Parent comment

Re:The SeL4 Foundation: What and Why by h91wka on Tuesday April 07, 2020 @08:46AM (#22802649)
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 in N bytes.

If you remove infinite tape, you go from undecidable to "just" exponentially complex.

[ Parent | on HN ]
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.

[ Parent | on HN ]
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.
[ Parent | on HN ]