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.
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.
I'm a Rust fanatic but probably not an activist. I am curious about Ada / SPARK though.
From what I've seen, taking on SPARK means taking on full verification, close to what seL4 is doing. Doesn't that make it extremely difficult to use for larger projects? My understanding is that seL4 is an absolutely heroic effort.
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.
Certainly I don't seem to run into as many of them as I'm led to believe exists.
I am a “Rust activist” any day of the week. seL4 is awesome and amazing.
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.
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.
6 replies →
I'm a Rust fanatic but probably not an activist. I am curious about Ada / SPARK though.
From what I've seen, taking on SPARK means taking on full verification, close to what seL4 is doing. Doesn't that make it extremely difficult to use for larger projects? My understanding is that seL4 is an absolutely heroic effort.
2 replies →
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.
https://discuss.haiku-os.org/t/replace-c-code-with-rust/6753
https://github.com/seL4/seL4/issues/487
Oh man, these are great.
Check out 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 as well. Reading the source code, it is mainly unsafe blocks and assembly. :| Who would have thought?
Love that discussion on the Haiku board.