Should I choose Ada, SPARK, or Rust over C/C++? (2024)

Original Article ↗ Hacker News Discussion ↗

Project context & basic advice

  • For personal projects: try several languages and see what feels right.
  • For work: follow existing company standards, tooling, and certification processes.

Safety-critical software: language vs process

  • Multiple commenters stress that high assurance comes primarily from process (requirements traceability, DO‑178C, MC/DC coverage, toolchains) rather than language alone.
  • Safety‑critical C is written in a very constrained style (no dynamic memory, minimal pointer arithmetic, heavy static analysis, formal tools like AbsInt).
  • Others argue that if a language can eliminate whole classes of bugs (UB, memory issues) by construction, it’s a clear win over relying solely on discipline and after‑the‑fact tools.

Ada/SPARK vs Rust vs C/C++

  • Pro‑Ada/SPARK points:
    • Strong, expressive type system (range‑constrained scalars, non‑zero/non‑integer array indices, domain‑specific types) encourages modeling problem domain rather than hardware.
    • SPARK can prove absence of certain runtime errors (buffer overflows, overflow, some functional properties) via contracts and static analysis.
    • You can freely mix SPARK and “plain” Ada in one project.
  • Skeptical views:
    • Similar invariants can often be enforced in Rust or C++ with types, assertions, and libraries.
    • Debate over whether SPARK’s proofs are fundamentally different from careful runtime checks and rich type systems.
    • Questioning how much formal proof really buys you when inputs are uncontrolled.
  • Rust discussion:
    • “Safe Rust” (outside unsafe) enforces memory safety and data‑race freedom, but that’s only one part of functional safety.
    • Some see Rust’s strong types and lifetimes as helpful for correctness; others find the type system overcomplex and empirically not clearly defect‑reducing.

Maintainability, adoption, and ecosystem

  • Ada is perceived as harder to maintain mainly for social reasons: few new developers, poor PR, little presence in mainstream domains (web, cloud, etc.).
  • Rust and Swift are seen as more “mainstream‑track” choices; Swift praised for C/C++ interop but criticized as bloated and syntactically fussy.

Broader language and culture notes

  • Some propose C++20, Zig, D, or staying with C++ if processes are strong.
  • Others push back on “just get better at C/C++” as unrealistic given long‑term defect history.
  • Debate over operator overloading, type redefinitions, and “taste” in language communities.