That comparison is nonsensical and you know it. You can delete all the comments and have the same guarantees about what the code does (none). You can’t write a kernel without some formal verification tool and then claim that it adheres to the specification.
Oh, I see. You said that it is “written in C”, and then later denied the claim that it is also written with that formal verification language. If you delete those annotations it will still adhere to the specification,[1] but it’s still false that it was purely written in C—your statement that “there are formally verified security guarantees” in fact relies on the existence of that proof code.
But fine. With that kind of dishonesty I could claim that the Linux kernel is written in nothing: I have compiled it and deleted the source code. Look ma, it’s no-code kernel.
[1] Kind of a bummer though that you cannot change any of the C code any more now that the verification code is gone.
Jesus Christ. It's not like most c programs arent already written in another language like make or cmake. By your standards none but the most trivial of hello world a.out c programs are c programs.
