Any kind of practical OS would contain code of unpractical amounts to manually review and audit. That's not to mention the argument that any software of a LOC

Any kind of practical OS would contain code of unpractical amounts to manually review and audit. That's not to mention the argument that any software of a LOC count of higher than some number is impossible to audit because of complex state handling. Rice's Theorem applies to your brain too, probably, to some extent. Idk about purely functional Haskell though.