I don't know Ada; care to explain why its definition of safety is broader than Rust?
I agree Rust's safety is very clearly (and maybe narrowly) defined, but it doesn't mean there isn't focus on general correctness - there is. The need to define safety precisely arises because it's part of the language (`unsafe`).
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)
with Ada.Text_IO; use Ada.Text_IO;
procedure Restricted_Number_Demo is
-- Define a restricted subtype of Integer
subtype Small_Positive is Integer range 1 .. 100;
-- Define a restricted subtype of Float
subtype Probability is Float range 0.0 .. 1.0;
-- Variables of these restricted types
X : Small_Positive := 42;
P : Probability := 0.75;
begin
Put_Line("X = " & Integer'Image(X));
Put_Line("P = " & Float'Image(P));
-- Uncommenting the following line would raise a Constraint_Error at runtime
-- X := 200;
end Restricted_Number_Demo;
I agree Rust's safety is very clearly (and maybe narrowly) defined, but it doesn't mean there isn't focus on general correctness - there is. The need to define safety precisely arises because it's part of the language (`unsafe`).