Messages in this thread | | | Date | Fri, 4 Sep 1998 10:23:07 +0200 | From | Martin Mares <> | Subject | Re: [OFFTOPIC] Re: Virtual Machines, JVM in kernel |
| |
> That was precisely my point: you can have a "proof" which claims "there are > no buffer overruns in this code", but you can't verify that proof when > working in C.
Why? You can have a C program for _generating_ proofs (given that, you would be able to solve the Halting problem), but I see no reason for verification of finite proofs about Turing machines being impossible in Turing-complete languages.
Have a nice fortnight -- Martin `MJ' Mares <mj@ucw.cz> http://atrey.karlin.mff.cuni.cz/~mj/ Faculty of Math and Physics, Charles University, Prague, Czech Rep., Earth "ebius tagline. This is a moebius tagline. This is a mo ..."
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/faq.html
| |