> I suspect, though, that memory safety is one of the most important kinds of safety.
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 & ";");
The above is perfectly safe because the constraint imposed prohibits the SQL-injection... and you can even enforce something like SQL_Escaping:
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;
> The tool would have to be pretty damn good. And also not introduce business risk or at the very least a minimal business risk.
That is actually quite possible.
Ada is in a really good place as far as that goes: imagine the cost of writing an IDE (to include compiler) for, say, Ada, PL/SQL, and VHDL -- given the common lineage, you could make a custom internal representations (IR), where each language has a 'Subtype' constraint for its particularity (e.g. `Subtype Ada_IR is General_IR with Dynamic_Predicate => Is_Common(Ada_IR) or Is_Ada(Ada_IR);`, and so on for PL/SQL and VHDL), make these IRs with SPARK proving, as you implement PL/SQL and its query-engine also implement SPARK's proof-tools and SMT-interfaces, proving it as you go, next implement and prove code-gen/HW-synth.
Now, put the IDE source through the IDE, and BAM! Now you have a proved IDE+compiler for Ada, PL/SQL, and VHDL giving you a very solid platform. (Also, as you would have a DB-engine onboard, you could populate the IDE with templates and run a query like: SELECT Name, Code FROM Entities WHERE Purpose LIKE “%SCSI%”;... or SELECT Name, Purpose FROM Algorithms WHERE Purpose LIKE “%SORT%” AND Ω <= log_2;.)
Memory management in Ada is such that you need pointers (and the heap) far, far less than in other languages: the language allows the return of values to objects of unconstrained subtypes to provide the constraints; example:
Text : Constant String := Read_Chapter( Book );
Additionally, nesting DECLARE blocks and subprograms allows a fairly fine-tuned memory-usage/cleanup using the stack. The above example could, for example, be part of an outer DECLARE block, which has an inner DECLARE, perhaps with "Paragraphs : Constant String_Vector := Get_Paragraphs( Text );" in its declarative region and "For Paragraph of Paragraphs loop" in its body... as soon as the block is exited, the stack is popped, reclaiming the used memory. This, in turn, means that the need for heap allocation is greatly reduced.
The type-system and forced spec/implementation split both work well to catch errors; you can go further with SPARK [proving] and using Pre- and Post-conditions, type-invariants.
The items "A serious take on a contract-based language" & "A language with semantic relations" are covered pretty nicely by Ada's SPARK subset/tools... and the really great thing is that the "aspects" are part of the code and don't "go stale" like annotated comments do.
> The C language also has a stable ABI, which is basically the ffi for most languages,
C is honestly terrible to target/use as FFI, doing so precludes doing things correctly, or more advanced things like... say arrays that "know their own length" or numeric-types that are range-constrained.
> Those don't need astral and can be passed through C ABI just fine.
No, they can't.
If you're passing a "Positive" through C's ABI you lose the fact that the value can be neither negative, nor zero. (Unless you mean "passed through" as in, "not mangled", but this is setting the bar so low as to be laughable.)
You are right; it's because the "modern" CI/CD is ill-designed, thanks in part to being "generalized" to handle text and "generalized" tools like C compilers and makefiles... instead of, you know, working in the actual problem-space.
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:
The above is perfectly safe because the constraint imposed prohibits the SQL-injection... and you can even enforce something like SQL_Escaping: