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.
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.
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.
You are right. I just plain don't care. Maybe I am misinformed. Maybe you are misunderstanding my requirements. Either way, it doesn't matter.
You seem to be missing the point - there is an entire ecosystem of things built in Rust, a community of developers using it in related fields to where I am working, and a vast store of experience and knowledge to draw upon.
Outside of aviation or defense, does Ada have that? No, it does not.
That is why no one uses it.
PS: This subthread started when someone made an assumption that Rust activists would pounce on this for not being written in Rust. I chimed in to say that, as a "rust activist" seL4 is actually pretty cool and that's fine. Then you butted in preach the Ada gospel. Not a good look.
> Outside of aviation or defense, does Ada have that? No, it does not.
> That is why no one uses it.
Both of these statements are false as well.
(I only made this response because you keep spreading misinformation about a language you know nothing about, self-admittedly, and demonstrably. Not a good look. Neither is your response to you being corrected. If you do not care, at least stop spreading bullshit so confidently about a language you do not know at all.)
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.
Ada is very scalable, suitable for everything from blinking LEDs on an AVR microcontroller board to controlling interplanetary spacecraft. Similarly, SPARK can be used incrementally, proving lower level or critical parts first.
How does this SPARK/non-SPARK mix compare to Rust's safe/unsafe mix though, in terms of both safety and pragmatism for larger non-interplanetary software? Like, for creating a CLI tool, a GUI application, a game, a web server?
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.
Rust is supported by the [seL4 Microkit](https://docs.sel4.systems/projects/rust/), which is the core framework enabling LionsOS. LionsOS can currently run components written in Rust, and there are some WIP drivers written in Rust in the seL4 Device Development framework (judging from pull requests).
At least someone hasn't complained about it being 'unix like', always without defining what the non-unix-like OS they want would look like, or where the software to run on it would come from.
First, we could start by what UNIX authors did after they considered UNIX done, looking at Plan 9 and Inferno.
Then there are the OSes already done during the 1960 and 1970 outside Bell Labs, as possible ideas.
As from where the software would come from, if we keep recicling UNIX, we will keep getting UNIX regardless of whatever cool features the OS might offer, as most developers are lazy.
Hence why it is great that while Apple and Google OSes have some UNIX there, bare bones POSIX apps will hardly make it into the store.
Yes, I think most of us are clear that seL4 isn't Unix. But people continue to complain that anything with a Posix layer is Unix-like, and therefore somehow 'bad'. My point was that virtually everyone who complains about this never, ever explains what would have been better to implement, just that it should have been different.
… except that Rust’s compiler has been qualified for several safety critical standards, with more to come, and has several formal verification tools as well. Amazon even has placed bounties (and paid some) for proving things about the standard library.
Rust is not as immature or evolving in the ways you imply.
Miri is not really a formal verification tool. It is more of a runtime sanitizer.
And it's because Rust's "no undefined behavior" is for safe Rust. Miri is used dynamically at runtime to catch undefined behavior in the unsafe superset.
Finally, Rust's safety guarantees relate to memory safety only. There's a lot more properties you'd want to prove about programs, some safety related in a broader sense, some totally unrelated to safety concerns.
By using some proof tools, you can find some of it.
It is technically impossible to find 100% of it at compile time because some of the finer details about what is UB are not nailed down 100% yet. But those are generally pretty fine corner cases, and one of the goals of those definitions is to not invalidate code as written.
