|
Rust’s built-in notion of safety is intentionally focused on memory + data-race properties at compile time. logic, timing, and determinism are left to libraries and design. Ada (with SPARK & Ravenscar) treats contracts, concurrency discipline, and timing analysis as first-class language/profile concerns hence a broader safety envelope. You may choose to think from safety guarantee hierarchy perspective like
(Bottom = foundation... Top = highest assurance) Layer 6: FORMAL PROOFS (functional correctness, no RT errors)
Ada/SPARK: built-in (GNATprove)
Rust: external tools (Kani, Prusti, Verus) Layer 5: TIMING / REAL-TIME ANALYSIS (WCET, priority bounds)
Ada: Ravenscar profile + scheduling analysis
Rust: frameworks (RTIC, Embassy) Layer 4: CONCURRENCY DETERMINISM (predictable schedules)
Ada: protected objects + task priorities
Rust: data-race freedom; determinism via design Layer 3: LOGICAL CONTRACTS & INVARIANTS (pre/post, ranges)
Ada: Pre/Post aspects, type predicates (built-in)
Rust: type states, assertions, external DbC tools Layer 2: TYPE SAFETY (prevent invalid states)
Ada: range subtypes, discriminants
Rust: newtypes, enums, const generics Layer 1: MEMORY SAFETY & DATA-RACE FREEDOM
Ada: runtime checks; SPARK proves statically
Rust: compile-time via ownership + Send/Sync |