Yeah - Ada has stuff like range types. So you can embed (some) function contracts into the type system.
I suspect, though, that memory safety is one of the most important kinds of safety. Especially if modern systems are going to be multi-threaded.
I don't. It seems to me like "memory-safety" is a response to the legacy of C and "C-compatibility) WRT poor behavior/respect of types; example: int/address punning, int/boolean punning, array/pointer punning, etc. (NUL-terminated stings could fit here, too as they're a consequence of C's address/array confusion.)
Contrary to this, would be correct typing. Consider SQL-injection and how the "best practice" is to never take data from the user... well we can take data from the user AND ensure there's no possibility of injection:
Subtype Numeric is String
with Dynamic_Predicate => (for all C of Numeric => C in '0'..'9'),
Predicate_Falure => raise Constraint_Error with "'" & Numeric &"' is not numeric.";
--...
Count : Numeric renames Get_User_Value;
--...
return Query("SELECT \* FROM Some_Table WHERE Count=" & Count & ";");
PACKAGE Example IS
-- The only way to get a value of ESCAPED_STRING is via calling Create.
Type Escaped_String is private;
Function Create( X:String ) return Escaped_String;
PRIVATE
Type Escaped_String is new String;
Function Create( X:String ) return Escaped_String is
( SQL_Escape(X) );
END Example;I don't agree, at least in the context of safety that Ada is typically mentioned in. Safety in this context is generally about human lives.
Memory safety is by far the most important kind of safety against exploits. Because memory safety bugs lead to arbitrary code execution and a total security breakdown.
However, where Ada is used most often - safety-critical and realtime systems in airplanes or medical equipment and such - most of the code is written for embedded systems. The attack surface is generally miniscule if any. The vast majority of issues that these contexts face I reckon are unit conversion errors, off-by-one errors, type overflows and logic errors.
The Rust static type system is actually not that rich for enforcing compile time constraints on values and states. It appears rich compared to C or Java or Go or something, but it's not that expressive even compared to languages in similar spaces like Scala or F# or even C++'s (rather terrifying) template system.
This has advantages and disadvantages. But for the kind of thing we're talking about, there's some disadvantages. There are things a richer type constraints system could offer beyond even the 'range' constraints other people in this thread are referring to.
e.g. I work on a (embedded-space) application that has a bunch of state machines in it. We naturally use Rust enums to describe these states. How nice it would be if Rust's enum system was rich enough to be able to describe and enforce the valid state transitions rather than just the set of possible states. There are various ways to try and approximate this (I've seen a few articles), but on the whole they're rather awkward and full of holes.
Also the verbosity of Ada's syntax looks painful to write but actually pretty nice to read. This has got to have lots of value for paranoid organizations.
I've seen plenty of terse and impenetrable Rust code, especially stuff that makes heavy use of rich static type action or funky things like GATs, etc.
I'm assuming you're referring to type state machines, where you have one struct per state and the only way to translate from one state to the next is through method calls. Defining these is quite verbose (unless you rely on macros) but how is it full of holes?
You're right macros could make this more pleasant. I still think it's quite unergonomic.
But yes, I probably should have said "awkward and/or full of holes" instead of and