> if you're program is anywhere near undecidability, it has no business being in the kernel.

who the hell cares just about "the kernel" (whatever kernel that is) ? I write native desktop applications and they are completely unverifiable.