Never use Float or Integer

If you've spent time writing C or C++, you know how easy it is to reach for int or float when declaring a variable. They are the workhorses of numeric programming: versatile, familiar, and always there when you need them. But that versatility comes with a hidden cost: the compiler has absolutely no idea what your numbers mean, and that means it cannot help you when you make a mistake.

Ada takes a different philosophy. Types carry meaning, and meaning prevents bugs. This post explores why you should almost never use Ada's built-in Float or Integer types directly and what to use instead.

When designing embedded or cyber-physical systems, the ranges of input and output signals are typically known. Sensors offer only a fixed range, and actuators are similarly restricted. Including these ranges in the input and output types of the system makes a lot of sense from an engineering perspective and prevents problems at the source.

The Problem with Generic Types

Consider a simple flight management system written in C. You are tracking aircraft speed and altitude:

float speed    = 250.0;
float altitude = 35000.0;

// Somewhere later...
speed = altitude;  // Oops. The compiler doesn't care.

The compiler compiles this happily. Both variables are float, after all. But you have just assigned an altitude in feet to a speed in knots—a logical catastrophe that may not surface until your program is running in production (or in the air).

The same trap exists with integers:

int passengers = 180;
int fuel_kg    = 42000;

fuel_kg = passengers;  // Compiler: fine by me!

C and C++ have no mechanism to distinguish between these. From the type system's point of view, a passenger count and a fuel load are the same thing: a number.

One could design a custom type through a class in C++, but that is a very heavyweight approach requiring additional work for the developer. The same limitation applies to Rust.

Ada's Answer: Define Types That Reflect Your Domain

Ada encourages you to define a distinct type for every distinct concept in your program. These are not just aliases or typedefs—they are genuinely incompatible types, and the compiler enforces that incompatibility.

type Speed_Knots   is new Float;
type Altitude_Feet is new Float;
type Passenger_Count is new Integer;
type Fuel_Kg         is new Integer;

Now, attempting the accidental assignments from above becomes a compile-time error:

Speed    : Speed_Knots   := 250.0;
Altitude : Altitude_Feet := 35000.0;

Speed := Altitude;  -- ERROR: expected type Speed_Knots, got Altitude_Feet

The compiler caught your bug before a single line of machine code ran. This is the core promise of Ada's type system: the more precisely you describe your data, the more the compiler can verify your logic.

And Types Are Just The Beginning

This article will continue with a detailed description of the benefits of the type system in Ada, complete with instructions on how to evaluate this easily in your current native development environment as well as on a Raspberry Pi Pico.

After reviewing the type system, we will briefly touch on additional extended capabilities of Ada to statically, at compile-time, prove the absence of runtime errors as well as prove functional correctness through its SPARK language subset.

Adding Range Constraints

Defining named types is just the beginning. Ada also lets you bake valid value ranges directly into your types. These constraints can be checked at compile time (when the value is a constant) or at runtime (with no extra code needed from you):

type Speed_Knots     is new Float range 0.0 .. 1000.0;
type Altitude_Feet   is new Float range 0.0 .. 60_000.0;
type Passenger_Count is new Integer range 0 .. 853;   -- Airbus A380 max
type Fuel_Kg         is new Integer range 0 .. 320_000;

Now the types do not just express what a value represents—they also express what values are valid. Assign -50.0 to a Speed_Knots and Ada raises a Constraint_Error. No extra validation logic, no unit tests needed to cover that case, and no undefined behavior as you would get with an integer overflow in C.

Compare that with C, where a negative speed is just a negative float. You would need to write your own checks, remember to call them everywhere, and hope nobody introduces a code path that bypasses them.

Subtypes for Specialisation Without New Types

Sometimes you want to narrow a type further without creating a fully incompatible new type. Ada's subtype is perfect for this:

subtype Cruising_Speed is Speed_Knots range 400.0 .. 900.0;
subtype Low_Altitude   is Altitude_Feet range 0.0 .. 10_000.0;

A Cruising_Speed is still a Speed_Knots, so you can use them interchangeably where a Speed_Knots is expected—but any attempt to store a value outside the cruising range will be caught. This is useful for expressing the different "modes" or "states" that a value can be in, without sacrificing type compatibility.

A More Complete Example

Here's a short Ada program that demonstrates these ideas together:

with Ada.Text_IO; use Ada.Text_IO;

procedure Flight_Data is

   type Speed_Knots     is new Float range 0.0 .. 1000.0;
   type Altitude_Feet   is new Float range 0.0 .. 60_000.0;
   type Fuel_Kg         is new Integer range 0 .. 320_000;
   type Passenger_Count is new Integer range 0 .. 853;

   subtype Cruising_Speed    is Speed_Knots range 400.0 .. 900.0;
   subtype Cruising_Altitude is Altitude_Feet range 25_000.0 .. 45_000.0;

   Current_Speed    : constant Cruising_Speed    := 550.0;
   Current_Altitude : constant Cruising_Altitude := 35_000.0;
   On_Board         : constant Passenger_Count   := 312;
   Fuel_Remaining   : constant Fuel_Kg           := 58_000;

begin

   -- This would be a compile error:
   -- Current_Speed := Current_Altitude;

   -- This would raise Constraint_Error at runtime:
   -- Current_Speed := 1_200.0;

   Put_Line ("Speed: " & Current_Speed'Image & " knots");
   Put_Line ("Altitude: " & Current_Altitude'Image & " feet");
   Put_Line ("Passengers: " & On_Board'Image);
   Put_Line ("Fuel: " & Fuel_Remaining'Image & " kg");

end Flight_Data;

Every variable has a type that encodes both its meaning and its valid range. A future developer reading this code learns not just that Current_Speed is a number—they learn that it is a speed measured in knots, and that it must be between 400 and 900 of them.

What About Performance?

A common concern from C and C++ developers is whether all this type checking costs performance. The answer is: almost never.

Range constraints that can be enforced at compile time are eliminated entirely—the compiler sees that the constant fits and generates no check. Constraints on variables introduce a comparison instruction, which modern CPUs can handle very efficiently. Meanwhile, you have eliminated whole classes of bugs that would otherwise require expensive runtime validation, defensive checks, or—worse—debugging sessions.

Ada compilers like GNAT can also generate code with checks disabled for release builds (-gnatp). However, the Ada philosophy generally favours leaving them on.

Try It Yourself with Alire

The fastest way to run these examples is with Alire (pronounced like "a-leer"), Ada's modern package manager and build tool. If you have used Cargo in Rust or npm in JavaScript, Alire will feel familiar.

Install Alire by downloading the binary for your platform from alire.ada.dev. It bundles its own GNAT toolchain, so you do not need to install a compiler separately.

Once installed, creating and running a new Ada project is three commands:

alr init --bin flight_data   # create a new executable project
cd flight_data
alr run                      # build and run in one step

Alire creates a src/flight_data.adb file—drop in the Flight_Data procedure from the example above, then run alr run to see it in action. To deliberately trigger a Constraint_Error, uncomment the out-of-range assignment and rebuild; you will see exactly where and why it failed.

Alire also gives you access to the full Alire Index, a curated catalogue of Ada libraries—everything from cryptography and networking to embedded runtimes. Need a library? It's:

alr with <crate-name>

That is it. No manual linker flags, no header paths to chase down. For a C++ developer used to fighting build systems, this part alone is worth the price of admission.

Running Ada on a Raspberry Pi Pico

Ada's strong typing is just as useful on a microcontroller as on a desktop—arguably more so, because there is no operating system to catch mistakes. The flight_data.adb file from the example above runs on the Pico unchanged; only the build configuration differs.

Start from the same project you created earlier, then add the ARM toolchain and Pico board support package:

cd flight_data
alr toolchain --select           # choose arm-elf when prompted
alr with pico_bsp                # pulls in the RP2040 HAL, BSP, and light runtime

Then open flight_data.gpr and add two lines inside the project declaration to tell gprbuild to target ARM rather than the host machine:

for Target use "arm-eabi";
for Runtime ("Ada") use "light-cortex-m0p";

Your source file does not need to change at all. Build with:

alr build

This produces a flight_data.uf2 file in the build output directory. To flash it, hold the BOOTSEL button on the Pico while plugging it into USB—it mounts as a mass storage device. Drag the .uf2 file onto it, and the Pico reboots and runs your program. The Put_Line output will appear on UART0 (pins GP0/GP1), which you can read with any serial monitor at 115200 baud.

To switch back to a native build, remove the pico_bsp dependency and restore the native toolchain:

alr with --del pico_bsp
alr toolchain --select         # choose gnat_native when prompted

The same source file, two targets.

One important difference from desktop Ada: the Pico's light runtime has no exception propagation. A range violation that would raise Constraint_Error on your laptop will instead trigger a hard fault trap on the Pico—the processor halts. In practice, this is fine for embedded code (a controlled stop is better than a corrupted state), but it is worth knowing when debugging. You can attach a debugger via the Pico's SWD pins and a Picoprobe to inspect exactly where the trap occurred.

SPARK: When the Compiler Proves Your Program Correct

Strong typing and range constraints are powerful, but they still leave a category of bugs untouched: logical errors that are perfectly type-correct but functionally wrong. A function that returns the right type but the wrong value will sail past the compiler.

This is where SPARK comes in. SPARK is a formally verifiable subset of Ada, supported by the GNATprove tool (available from Alire via alr with gnatprove). In addition to proving statically the correctness of types and ranges, SPARK can mathematically prove that your program cannot exhibit certain classes of error—buffer overflows, division by zero, invalid array accesses, unintended data flow—without ever executing the code.

The key mechanism is contracts: preconditions, postconditions, and invariants that you attach to your subprograms and types. Here is the flight-data example extended with a SPARK contract:

procedure Set_Speed (S : in out Speed_Knots; New_Value : Speed_Knots)
  with
    Pre  => New_Value >= 0.0 and New_Value <= 1000.0,
    Post => S = New_Value;

GNATprove reads these contracts and attempts to prove—statically, at build time—that every call site satisfies the precondition, and that the body of the subprogram actually guarantees the postcondition. If it cannot prove something, it tells you exactly which condition failed and on which line, giving you a precise target for either fixing the code or adding the missing invariant.

The practical result is that SPARK programs can achieve the software assurance levels required by standards such as DO-178C (avionics), ISO 26262 (automotive), EN 50128 (rail), and IEC 61508 (functional safety)—domains where a runtime bug is not just costly but potentially fatal. The European train control system, parts of the F-35 flight software, and critical components of commercial aircraft fly on SPARK-verified Ada, as do core parts of the software on NVIDIA SoCs.

For a C or C++ developer, the mental model is this: SPARK takes the type discipline described in this post and extends it all the way to correctness proofs. You are not just telling the compiler what your data is—you are telling it what your code must do, and the tool verifies that it actually does it.

A good entry point is the SPARK documentation on learn.adacore.com, which walks through verification from simple range proofs through to full functional correctness.

The Mindset Shift

Moving from C or C++ to Ada's type discipline is less a syntactic change than a conceptual one. In C, you tend to think: "what is the right primitive type to store this?". In Ada, you think: "what is this value, and what are the rules that govern it?"

Once you start defining types that reflect your domain, a surprising thing happens: your code becomes self-documenting, your interfaces become harder to misuse, and your compiler becomes an active collaborator rather than a passive translator.

So the next time you are tempted to write:

Speed : Float := 0.0;

Ask yourself what that Float actually represents—and give it a name.

Further Reading

Ada's type system goes even further than what is covered here. Topics worth exploring next include:

• Modular types - integers that wrap around at a specific power of two, ideal for bit manipulation.
• Fixed-point types - exact decimal arithmetic without the rounding surprises of floating point.
• Tagged types - Ada's approach to object-oriented programming with full type safety.
• Ada Contracts (Pre, Post, Type_Invariant) - attaching formal correctness conditions directly to your types and subprograms.
• Generic types - Ada's generics let you write type-safe, reusable algorithms and data structures parameterised over any type, without sacrificing the strong typing guarantees described in this post. Think C++ templates, but with well-defined semantics and no header-file surprises.

The best place to start is learn.adacore.com, which offers free, interactive Ada courses ranging from a beginner introduction through to advanced topics in formal verification.

Sign in