Hacker News Reader

This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent.

The problem I take with the literature is that it does not say that it is free of certain classes of bugs. The wording implies that it is completely bug-free. As any software developer knows, bug-free software does not exist.

Furthermore,

You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them.

they claim they have proven that their kernel is completely bug-free. They say they have proved this under the assumption that the assembly code was written correctly. It seems that what they have claimed is: we have proven our kernel is correct with a proof that assumes that the code is written correctly. The logical flaw in this is obvious.

I don't take issue with claims of correctness, given that they are precise about what they have proven. I do take issue with inflated claims ("bug-free" vs. "free of bugs from this specific class of bugs") for marketing purposes.

View on HN