6 ms·

I'm trying to picture in my mind a person who is a fan of Rust and somehow against an OS with a formally-verified kernel no matter the language. I'm not having

I'm trying to picture in my mind a person who is a fan of Rust and somehow against an OS with a formally-verified kernel no matter the language. I'm not having much success.

fooker 10mo ago
I see you have not met a lot of Rust activists.
- aloha2436 10mo ago
  Certainly I don't seem to run into as many of them as I'm led to believe exists.
- pppppiiiiiuuuuu 10mo ago
  It's funny how people always allude to fanatical Rust developers in the most tangential threads, but they never actually turn up and demand we rewrite the entire Kernel in Rust or whatever terrible takes they're alleged to have.
  - fooker 10mo ago
    https://discuss.haiku-os.org/t/replace-c-code-with-rust/6753 https://discuss.haiku-os.org/t/replace-c-code-with-rust/6753 https://github.com/seL4/seL4/issues/487 https://github.com/seL4/seL4/issues/487
    - aduty 10mo ago
      Love that discussion on the Haiku board.
    - johnisgood 10mo ago
      Oh man, these are great. Check out https://github.com/ansuz/RIIR/issues/ https://github.com/ansuz/RIIR/issues/ for more. Gosh... and people on HN tell us that they have yet to meet a Rust fanatic. Just look around the GitHub Issues I linked. --- BTW I stumbled upon https://github.com/r9os/r9 https://github.com/r9os/r9 as well. Reading the source code, it is mainly unsafe blocks and assembly. :| Who would have thought?
- adastra22 10mo ago
  I am a “Rust activist” any day of the week. seL4 is awesome and amazing.
  - johnisgood 10mo ago
    Thoughts on Ada / SPARK? Why are you not using Ada / SPARK considering it has such a neat type system, pre- and post-conditions, formal verification, and so forth. It has built-in concurrency constructs as well and it helps you avoid deadlocks and race conditions.
    - adastra22 10mo ago
      Well, why should I? Does it bring anything else to the table? After 50 years it doesn’t have the momentum rust has, or the tooling and ecosystem. In any case, it really isn’t comparable. It doesn’t have a borrow checker, contracts are enforced at runtime not compile time, no move semantics and no smart pointers… I find it strange actually that there is always someone bringing up “what about Ada/SPARK?” in the comments when there aren’t even comparable.
      - deleted 10mo ago
        [deleted]
      - johnisgood 10mo ago
        You are wrong on all counts. It brings more to the table than Rust does. I have talked about this before, but here I go again (because your comment is full of misinformation). SPARK contracts are compile-time verified, not runtime. The GNATprove tool statically proves absence of runtime errors, buffer overflows, arithmetic overflow, and user-defined contracts (preconditions, postconditions, invariants) at compile time with zero runtime overhead. This is formal verification, not runtime checks. Ada has move semantics since Ada 2012 via limited types and function returns. Limited types cannot be copied, only moved. This is enforced at compile time. Build-in-place optimization eliminates unnecessary copies. Ada has smart pointers. Ada.Containers.Indefinite_Holders provides reference semantics, GNATCOLL.Refcount provides explicit reference counting, and controlled types (Ada.Finalization.Controlled) give you RAII-style resource management with deterministic finalization, effectively custom smart pointers. Search for "Ada smart pointers". Ownership/borrowing in SPARK: While not called a "borrow checker," SPARK's ownership model (Ada 202x, SPARK RM 3.10) provides compile-time verification of pointer safety, including ownership transfer, borrowing (observed/borrowed modes), and prevents use-after-free and aliasing violations. The verification is actually more comprehensive than Rust because it proves full functional correctness, not just memory safety. Certification: Ada/SPARK is DO-178C certified for avionics, used in safety-critical systems (Airbus, Boeing, spacecraft), and has Common Criteria EAL certification. Rust has no comparable certification history for high-assurance systems. The tooling argument is partially valid. Rust has better modern tooling (although Ada now has a proper package manager) and a more lively ecosystem. But claiming Ada lacks move semantics, or smart pointers is factually incorrect, and SPARK proves what Rust's borrow checker only approximates, and does so with mathematical proof, not heuristics. Why should you care? You answer that, but I think you may be right, you are just a Rust activist. What I find strange is the confidence with which you make verifiably and demonstrably incorrect statements about Ada, a language you clearly have not studied.

I'm trying to picture in my mind a person who is a fan of Rust and somehow against an OS with a formally-verified kernel no matter the language. I'm not having much success.

fooker 10mo ago

I see you have not met a lot of Rust activists.

aloha2436 10mo ago
Certainly I don't seem to run into as many of them as I'm led to believe exists.
pppppiiiiiuuuuu 10mo ago
It's funny how people always allude to fanatical Rust developers in the most tangential threads, but they never actually turn up and demand we rewrite the entire Kernel in Rust or whatever terrible takes they're alleged to have.
- fooker 10mo ago
  https://discuss.haiku-os.org/t/replace-c-code-with-rust/6753 https://discuss.haiku-os.org/t/replace-c-code-with-rust/6753 https://github.com/seL4/seL4/issues/487 https://github.com/seL4/seL4/issues/487
  - aduty 10mo ago
    Love that discussion on the Haiku board.
  - johnisgood 10mo ago
    Oh man, these are great. Check out https://github.com/ansuz/RIIR/issues/ https://github.com/ansuz/RIIR/issues/ for more. Gosh... and people on HN tell us that they have yet to meet a Rust fanatic. Just look around the GitHub Issues I linked. --- BTW I stumbled upon https://github.com/r9os/r9 https://github.com/r9os/r9 as well. Reading the source code, it is mainly unsafe blocks and assembly. :| Who would have thought?
adastra22 10mo ago
I am a “Rust activist” any day of the week. seL4 is awesome and amazing.
- johnisgood 10mo ago
  Thoughts on Ada / SPARK? Why are you not using Ada / SPARK considering it has such a neat type system, pre- and post-conditions, formal verification, and so forth. It has built-in concurrency constructs as well and it helps you avoid deadlocks and race conditions.
  - adastra22 10mo ago
    Well, why should I? Does it bring anything else to the table? After 50 years it doesn’t have the momentum rust has, or the tooling and ecosystem. In any case, it really isn’t comparable. It doesn’t have a borrow checker, contracts are enforced at runtime not compile time, no move semantics and no smart pointers… I find it strange actually that there is always someone bringing up “what about Ada/SPARK?” in the comments when there aren’t even comparable.
    - deleted 10mo ago
      [deleted]
    - johnisgood 10mo ago
      You are wrong on all counts. It brings more to the table than Rust does. I have talked about this before, but here I go again (because your comment is full of misinformation). SPARK contracts are compile-time verified, not runtime. The GNATprove tool statically proves absence of runtime errors, buffer overflows, arithmetic overflow, and user-defined contracts (preconditions, postconditions, invariants) at compile time with zero runtime overhead. This is formal verification, not runtime checks. Ada has move semantics since Ada 2012 via limited types and function returns. Limited types cannot be copied, only moved. This is enforced at compile time. Build-in-place optimization eliminates unnecessary copies. Ada has smart pointers. Ada.Containers.Indefinite_Holders provides reference semantics, GNATCOLL.Refcount provides explicit reference counting, and controlled types (Ada.Finalization.Controlled) give you RAII-style resource management with deterministic finalization, effectively custom smart pointers. Search for "Ada smart pointers". Ownership/borrowing in SPARK: While not called a "borrow checker," SPARK's ownership model (Ada 202x, SPARK RM 3.10) provides compile-time verification of pointer safety, including ownership transfer, borrowing (observed/borrowed modes), and prevents use-after-free and aliasing violations. The verification is actually more comprehensive than Rust because it proves full functional correctness, not just memory safety. Certification: Ada/SPARK is DO-178C certified for avionics, used in safety-critical systems (Airbus, Boeing, spacecraft), and has Common Criteria EAL certification. Rust has no comparable certification history for high-assurance systems. The tooling argument is partially valid. Rust has better modern tooling (although Ada now has a proper package manager) and a more lively ecosystem. But claiming Ada lacks move semantics, or smart pointers is factually incorrect, and SPARK proves what Rust's borrow checker only approximates, and does so with mathematical proof, not heuristics. Why should you care? You answer that, but I think you may be right, you are just a Rust activist. What I find strange is the confidence with which you make verifiably and demonstrably incorrect statements about Ada, a language you clearly have not studied.