Skip to main content
Background image of Earth and satellite
Background image of Earth and astronaut

Ada Programming Language

A programming language for readable, correct, and performant software.
Get started with Alire, the Ada package manager.
Download Alire v2.0.2
Get Started
Download for Windows, macOS, Linux, AppImage, or others
with Ada.Text_IO;

procedure Main is
   type GUID is new String (1 .. 32)
     with Dynamic_Predicate =>
       (for all C of GUID => C in '0' .. '9' | 'a' .. 'f');

   ID_1 : constant GUID := "030000004c050000cc09000011810000";
begin
   Ada.Text_IO.Put_Line ("Reading from device " & String (ID_1) & "...");
end Main;
with Interfaces;

package Xoshiro128 with Pure, SPARK_Mode => On is
   use type Interfaces.Unsigned_64;

   type Generator is limited private;

   procedure Next (S : in out Generator; Value : out Interfaces.Unsigned_32)
     with Global  => null,
          Depends => (S => S, Value => S);

   procedure Reset (S : out Generator; Seed : Interfaces.Unsigned_64)
     with Global  => null,
          Depends => (S => Seed),
          Pre     => Seed /= 0;

private
   type Generator is array (0 .. 3) of Interfaces.Unsigned_32;
end Xoshiro128;
with RP.GPIO;
with Pico;

procedure Main is
begin
   Pico.LED.Configure (RP.GPIO.Output);
   loop
      Pico.LED.Toggle;
      delay 0.1;
   end loop;
end Main;
Ada

Readable, correct, performant

Express intent with explicitness, describe properties with predicates and pre/post conditions, and import C/C++ functions or intrinsics.
Readable

Express intent with explicitness and keywords over symbols and special structures.

Express concepts like meaning in integers. Use built-in design by contract with pre/post-conditions and invariants. Model problems with typechecks and range constraints.

Correct

Build with technology used in 40 years of reliability in planes, trains, and satellites.

Use the SPARK subset to formally verify part or all of your program, and integrate existing SPARK crates available in the Alire package manager.

Performant

Build native applications and take advantage of other libraries through binding to C and C++.

Use inline assembly or compiler intrinsics when you need it. Control resources with scope-based resource control (RAII) and your own memory allocators.

Set-up environment

Package manager + toolchain

Download the Alire package manager and install the compiler.
Download Alire
Download Alire v2.0.2.
Install toolchain
alr toolchain --select
Select gnat_native and gprbuild.
Start coding
Create a crate:
alr init --bin mycrate && cd mycrate
Build the crate:
alr build
Run your application
alr run
SPARK

From memory safety to functional correctness

Gradually adopt the SPARK subset to reach various levels of assurance. Higher levels take more effort, but give more benefits and stronger guarantees.
Validates code
Restricts Ada packages to the SPARK subset. Avoids side-effects in functions and parameter aliasing.
Checks initialization and data flow
No uninitialized variables are read or undesired access to globals occurs.
Proves the absence of run-time errors
No buffer and arithmetic overflow, division by zero, or values out of range, among others, can occur.
Ensures key integrity properties
Verifies integrity of data and valid state transitions.