https://ada-lang.io/

Skip to main content
Please thank Jay on HN or lobsters for announcing this website, which
is still work in progress! Thanks Jay! 
 
AdaAda
AdaGetting StartedReference ManualStyle Guide
 

Ada Programming Language

A programming language for readable, correct, and performant
software.
Get started with Alire, the Ada package manager.
 
Download Alire 1.2.1
 
Get Started
Download for Windows, macOS, Linux, AppImage, or others
Ada
SPARK
Embedded

1
with Ada.Text_IO;
2

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

8
   ID_1 : constant GUID := "030000004c050000cc09000011810000";
9
begin
10
   Ada.Text_IO.Put_Line ("Reading from device " & String (ID_1) & "...");
11
end Main;

1
with Interfaces;
2

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

6
   type Generator is limited private;
7

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

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

17
private
18
   type Generator is array (0 .. 3) of Interfaces.Unsigned_32;
19
end Xoshiro128;

1
with RP.GPIO;
2
with Pico;
3

4
procedure Main is
5
begin
6
   Pico.LED.Configure (RP.GPIO.Output);
7
   loop
8
      Pico.LED.Toggle;
9
      delay 0.1;
10
   end loop;
11
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 1.2.1.
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.
Valid SPARK
Restrict Ada packages to the SPARK subset. Avoids side-effects in
functions and parameter aliasing.
Initialization and correct data flow
No uninitialized variables are read or undesired access to globals
occurs.
Absence of run-time errors
No buffer and arithmetic overflow, division by zero, or values out of
range, among others, can occur.
Key integrity properties
Verify integrity of data and valid state transitions.
Learning

  * Tutorial
  * Learn Ada (by AdaCore)
  * Learn SPARK (by AdaCore)

Docs

  * Wikibook
  * Style Guide

Community

  * Gitter
  * Reddit
  * Telegram
  * Stack Overflow

More

  * Alire (Ada package manager)
  * Awesome Ada
  * News, by Ada Planet
  * GitHub

AltAlt
Copyright (c) 2022 and licensed under Apache 2.0 unless otherwise
noted, by the ada-lang-io developers. Built with Docusaurus.