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