Yes. And they could contain errors even without OS and hardware. And practice clearly shows it. Proofs are easier to make on the same abstraction level, aren't they?