You are wrong on all counts.<p>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).<p><i>SPARK contracts are compile-time verified</i>, 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.<p><i>Ada has move semantics</i> 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.<p><i>Ada has smart pointers</i>. 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".<p><i>Ownership/borrowing in SPARK</i>: 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. <i>The verification is actually more comprehensive than Rust because it proves full functional correctness, not just memory safety.</i><p><i>Certification</i>: 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.<p>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 <i>SPARK proves what Rust's borrow checker only approximates, and does so with mathematical proof, not heuristics.</i><p>Why should you care? You answer that, but I think you may be right, you are just a Rust activist.<p>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.<p>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.<p>Outside of aviation or defense, does Ada have that? No, it does not.<p>That is why no one uses it.<p>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.<p>> That is why no one uses it.<p>Both of these statements are false as well.<p>(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.)
Just want to say Thank You. May be thank you "again" because I remember I said this previously as well.<p>Every time I mention Ada on HN it is always the Rust people that claims it is irrelevant, especially when it is them who started only Rust can do X.<p>The unwritten rule of HN: You do not criticise The Rusted Holy Grail or the Riscy Silver Bullet.