4 ms·

seL4 also has the whole Isabelle/HOL theorem prover to verify its properties, so it's not quite right to claim it's written in C. If you can claim seL4 is "writ

by vore 4y ago

seL4 also has the whole Isabelle/HOL theorem prover to verify its properties, so it's not quite right to claim it's written in C. If you can claim seL4 is "written in C", you could equally claim that if the Rust compiler emitted C, you're writing a C program -- after all, a static type checker is just a shittier theorem prover.

throwawaymaths 4y ago
This is like saying <insert language with docstrings> is not actually writing in <lang> because you need whatever engine's target language (md, XML, whatever) to compile the docs.
- avgcorrection 4y ago
  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.
  - throwawaymaths 4y ago
    No, but if you change none of the code and only delete the annotations, it will still adhere to the spec.
    - avgcorrection 4y ago
      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.
      - throwawaymaths 4y ago
        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.

by vore 4y ago

throwawaymaths 4y ago

This is like saying <insert language with docstrings> is not actually writing in <lang> because you need whatever engine's target language (md, XML, whatever) to compile the docs.

avgcorrection 4y ago
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.
- throwawaymaths 4y ago
  No, but if you change none of the code and only delete the annotations, it will still adhere to the spec.
  - avgcorrection 4y ago
    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.
    - throwawaymaths 4y ago
      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.