Ada's type system allows you to separate the high-level specification of a type (which models a problem) and its low-level representation (size, alignment, bit/byte order, etc.). The language also requires explicit conversions for two different types even if their underlying representation on the hardware is the same.
Example 1:
type Byte_Count is range 1 .. 4
with Static_Predicate => Byte_Count in 1 | 2 | 4; -- Aspects are Ada 2012
type Component_Count is range 1 .. 4;
V1 : Byte_Count := 3; -- compiler error: expression fails predicate check
V2 : Component_Count := V1; -- compiler error: requires explicit conversion
For these two types I'm not really concerned about how they are represented by the hardware, but I could if I needed to.
Example 2:
Extra constraints added to some pre-defined types:
subtype String8 is String
with Dynamic_Predicate => String8'Length Even_Integer mod 2 = 0,
Predicate_Failure => "Even_Integer must be a multiple of 2";
Example 3:
Use big-endian for some network packets:
type Packet_Type is record
Header : Header_Type;
Data : Data_Type;
end record;
Low-level representation (placed in the private part of a package spec):
for Packet_Type use record
Header at 0 range 0 .. 255;
Data at 0 range 256 .. 1855;
end record;
for Packet_Type'Bit_Order use System.High_Order_First;
for Packet_Type'Scalar_Storage_Order use System.High_Order_First;
for Packet_Type'Size use 232 * System.Storage_Unit;