(1) encapsulation, realized in Ada by private types.

    Package Geometry is
       Type Point is private;
       Function  Create( X, Y : Integer ) return Point;
       Function  X( Object : Point ) return Integer;
       Function  Y( Object : Point ) return Integer;
       Procedure X( Object : in out Point; Value : Integer );
       Procedure X( Object : in out Point; Value : Integer );
    Private
       Type Point is record
          Data_X, Data_Y : Real:= 0.0;
       end record;
    
       Function  X     ( Object : Point ) return Integer is (Object.Data_X);
       Function  Y     ( Object : Point ) return Integer is (Object.Data_X);
       Function  Create( X, Y : Integer ) return Point   is
         ( Data_X => X, Data_Y => Y);
    End Geometry;

    Generic
       Type Item is private;
       One : Item;
       with "*"(Left, Right : Item) return Item is <>;
    Function Generic_Exponent( Base : Item; Exponent : Natural ) return Item;
    -- ...implementation
    Function Generic_Exponent( Base : Item; Exponent : Natural ) return Item is
     (case Exponent is
        when 0 => One,
        when 1 => Base,
        when 2 => Base*Base,
        when others =>
          -- Rule: X**2k = (X**k)**2; X**2k+1 = (X**k)**2 * X.
          (Generic_Exponent(Base, Generic_Exponent(Base, Exponent/2), 2)
            *  (if Exponent mod 2 = 1 then Base else One);
     );

    Type Temperature is range -40..2_000;
    Type Probe_Range is new Temperature range -20..200;

    (See above; note how we're depending on the type, a "one value", and a "multiply" operation.)

    Type Base is null record;
    Function Text(Object : Base) return String is ("[]");
    
    Type Color is ( Red, Green, Blue, Black, White );
    Type Colored_Thing is new Base with record
       Color_Data : Color := Red;
    end record;
    
    Function Text(Object : Colored_Thing) return String is
      ('[' & Color'Image(Object.Color_Data) & " ]");

    -- Gets text from user.
    Function Prompt return String; -- def elsewhere.
    -- Gets a previously saved object.
    Function Get( Name : String ) return Base'Class; -- def elsewhere.
    Unknown_From_User : Base'Class renames Get( Prompt );
    --...
    -- The following will print "[]" if it is BASE, and
    -- "[ COLOR ]" when COLORED_THING, replacing 'COLOR' with
    -- the textual representation/literal for the value.
    Ada.Text_IO.Put_Line( Unknown_From_User.Text );

For GNAT, these two pieces of documentation are instructive: https://docs.adacore.com/live/wave/gnat_rm/html/gnat_rm/gnat... https://gcc.gnu.org/onlinedocs/gcc-4.9.1/gnat_rm/FORM-String... (This second one is older documentation, but illustrates how platform-specific Form parameters could be used.)

    Ada.Text_IO.Create (
        File => File,
        Mode => Ada.Text_IO.Out_File,
        Name => "test.txt",
        Form => "shared=no"
      );

    Package Dependency is
       Package OS is
          Function Separator return String;
       End OS;
    End Dependency;
    -- ...
    Package Dependency is
       Package body OS is separate;
    End Dependency;

    -- Windows
    separate (Dependency)
    Package OS is
      Function Separator return String is ("\");
    End OS;

    -- Classic Mac
    separate (Dependency)
    Package OS is
      Function Separator return String is (":");
    End OS;

    -- VMS
    separate (Dependency)
    Package OS is
      Function Separator return String is (".");
    End OS;

    -- UNIX-like
    separate (Dependency)
    Package OS is
      Function Separator return String is ("/");
    End OS;

    Generic
      Type Index   is (<>);                                      -- Any discrete type.
      Type Element is limited private;                           -- Any non-discriminated type.
      Type Vector  is array(index range <>) of element;          -- An array-type of Element, indexed by Index.
      with Function "="(Left, Right: Element) return Boolean <>; -- Equal, defaulted.
      with Function "<"(Left, Right: Element) return Boolean <>; -- Less-than, defaulted.
    Function Generic_Sort( X : Vector ) return Vector;

    Function Sort is new Generic_Sort( Index => Integer, Element => Integer, Vector => Integer_Array, "<" => ">");

The best way to use Ada, IMO, is type-first: you define your problem-space in the type-system, then use that to solve your problem. -- Also, because Ada's foreign-function interface is dead easy, you could use imports to handle things in a manner more amiable to your needs/preferences, it's as simple as:

    Function Example (X : Interfaces.Unsigned_16) return Boolean
      with Import, Convention => COBOL, Link_Name => "xmpl16";

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;

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;.)

Also, being Ada-based, you could use Ada's Distributed Systems Annex to distribute portions of the IDE, and/or implement CI/CD as per https://users.ece.utexas.edu/~perry/work/papers/icsm87.pdf

    Text : Constant String := Read_Chapter( Book );

Here's an excellent presentation on Ada's memory management: https://archive.fosdem.org/2016/schedule/event/ada_memory/

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.

>

> There's a fair amount of C code that does just that and does it for a long time.

No, there isn't.

There can't be because of how arrays in C degenerate into pointers/addresses; see Walter Bright's "C's Biggest Mistake" -- here: https://www.digitalmars.com/articles/C-biggest-mistake.html

>> 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.)

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.