LEARN ADA DEEP DIVE

Learn Ada: From Zero to High-Integrity Master

Goal: To master the Ada programming language by building projects that leverage its core strengths: safety, concurrency, and reliability. You will learn to write robust code that is correct by construction, using Ada’s powerful type system, tasking, and contract-based programming.

Why Learn Ada?

In a world of memory-unsafe languages and complex concurrency libraries, Ada stands apart. It was designed from the ground up for large, long-lived, and mission-critical applications—think aerospace, railway control, medical devices, and financial systems. Learning Ada doesn’t just teach you a new syntax; it teaches you a rigorous approach to software engineering.

After completing these projects, you will:

Appreciate the power of a truly strong type system with subtypes and constraints.
Build complex concurrent applications with ease using Ada’s native tasking model.
Write code that is verifiable and robust using Design by Contract (Pre/Post conditions).
Structure large applications cleanly using Ada’s package system.
Understand the mindset required for building high-integrity software.

Core Concept Analysis

Ada’s philosophy is to detect errors as early as possible—preferably at compile time.

1. Packages: Encapsulation and Modularity

Everything in Ada is organized into packages. Each package has two parts, which are compiled separately:

Specification (.ads file): The public interface. It defines the types, variables, and subprogram signatures that are visible to the outside world. This is the “contract.”
Body (.adb file): The private implementation. It contains the implementation of the subprograms declared in the specification, as well as any private data or helper functions.

-- hello.ads (Specification)
package Hello is
   procedure Put_Line (Message : in String);
end Hello;

-- hello.adb (Body)
with Ada.Text_IO;
package body Hello is
   procedure Put_Line (Message : in String) is
   begin
      Ada.Text_IO.Put_Line (Message);
   end Put_Line;
end Hello;

2. Strong Typing and Subtypes: Correct by Construction

Ada’s type system is much stricter than C++’s or Java’s. More importantly, it allows you to create custom subtypes with built-in constraints. The compiler or runtime will then enforce these constraints for you.

-- Instead of just using "Integer" and hoping the value is right...
subtype Day_Of_Month is Integer range 1 .. 31;
subtype Hour_Of_Day  is Integer range 0 .. 23;

My_Day : Day_Of_Month;
My_Day := 32; -- Raises a Constraint_Error at runtime!

This catches a huge number of bugs automatically.

3. Tasks: Concurrency as a Language Feature

Unlike other languages that rely on external libraries (pthreads, std::thread), concurrency is built directly into the Ada language through tasks. Tasks are units of execution that run in parallel. They communicate safely using well-defined mechanisms.

task type Printer_Task; -- Defines a "class" of task

task body Printer_Task is -- The implementation
begin
   loop
      accept Print (Message : in String) do -- Rendezvous point
         -- Safely handle the print job
      end Print;
   end loop;
end Printer_Task;

My_Printer : Printer_Task; -- Creates a task instance
My_Printer.Print ("Hello, Concurrent World!"); -- Calls the entry

4. Design by Contract: Provable Code

Ada allows you to specify contracts on your functions, making your intentions explicit and verifiable.

Pre condition: Something that must be true before a subprogram is called.
Post condition: Something that must be true after a subprogram finishes.

function Sqrt (X : in Float) return Float with
   Pre  => X >= 0.0,
   Post => Sqrt'Result * Sqrt'Result is close to X;

When enabled, these contracts are checked at runtime. Even more powerfully, the SPARK language subset and gnatprove tool can use these contracts to mathematically prove the absence of certain runtime errors at compile time.

Project List

These projects are designed to introduce you to the core features of Ada in a logical progression. You will need an Ada compiler, like the GNAT toolchain, which is easy to install with Alire, the Ada package manager.

Project 1: Safe Units Conversion Library

File: LEARN_ADA_DEEP_DIVE.md
Main Programming Language: Ada
Alternative Programming Languages: N/A
Coolness Level: Level 2: Practical but Forgettable
Business Potential: 1. The “Resume Gold”
Difficulty: Level 1: Beginner
Knowledge Area: Strong Typing / Subtypes / Packages
Software or Tool: GNAT, Alire
Main Book: “Programming in Ada 2012” by John Barnes

What you’ll build: A simple Ada package for performing unit conversions (e.g., Celsius to Fahrenheit, kilometers to miles) in a type-safe way, preventing nonsensical operations like adding a temperature to a distance.

Why it teaches Ada: This project is a perfect introduction to Ada’s core strength: the type system. You will learn to stop thinking in terms of primitive types (Float, Integer) and start thinking in terms of problem-domain types (Temperature, Distance). This will immediately highlight how Ada prevents entire classes of bugs at compile time.

Core challenges you’ll face:

Defining distinct numeric types → maps to type Celsius is new Float;
Creating subtypes with constraints → maps to subtype Kelvin is Float range 0.0 .. Float'Last; to forbid temperatures below absolute zero
Writing conversion functions → maps to explicitly converting between your new types
Overloading operators → maps to defining what + means for two Distance types, while making it a compile error for a Distance and a Temperature

Key Concepts:

Packages: “Programming in Ada 2012” Ch. 7 - John Barnes
Derived Types and Subtypes: “Programming in Ada 2012” Ch. 5 - John Barnes
Operator Overloading: learn.adacore.com tutorials.

Difficulty: Beginner Time estimate: Weekend Prerequisites: Basic programming knowledge in any language.

Real world outcome: A reusable library package and a small demo program.

-- Using your library
with Ada.Text_IO; use Ada.Text_IO;
with Safe_Units.Temperatures; use Safe_Units.Temperatures;

procedure Temp_Demo is
   C : Celsius := 20.0;
   F : Fahrenheit;
   K : Kelvin;
begin
   F := To_Fahrenheit (C);
   Put_Line ("20C is " & F'Image & "F");

   -- K := C; -- This would be a compile-time error!
   K := To_Kelvin(C);
   Put_Line ("20C is " & K'Image & "K");

   -- F := F + C; -- This would also be a compile error!
end Temp_Demo;

Implementation Hints:

Create a package specification safe_units.ads. Inside, declare another package Temperatures.
In safe_units-temperatures.ads, define your types: type Celsius is new Float;, type Fahrenheit is new Float;.
Define a subtype for absolute zero: subtype Absolute_Float is Float range 0.0 .. Float'Last; type Kelvin is new Absolute_Float;.
Declare your conversion functions in the spec: function To_Fahrenheit(C : Celsius) return Fahrenheit;.
In the body (.adb file), implement the conversion formulas. Note that you will have to explicitly cast between types, e.g., Fahrenheit(1.8 * Float(C) + 32.0). This explicitness is a feature.

Learning milestones:

You have a working package for temperature conversions → You understand packages and functions.
The compiler stops you from adding Celsius to Fahrenheit → You understand distinct types.
The program raises a Constraint_Error if you try to create a negative Kelvin temperature → You understand subtypes.
You start modeling real-world quantities with specific types instead of generic numbers → You are thinking in Ada.

Project 2: Concurrent Traffic Light Simulation

File: LEARN_ADA_DEEP_DIVE.md
Main Programming Language: Ada
Alternative Programming Languages: N/A
Coolness Level: Level 4: Hardcore Tech Flex
Business Potential: 1. The “Resume Gold”
Difficulty: Level 2: Intermediate
Knowledge Area: Concurrency / Tasking / Synchronization
Software or Tool: GNAT, Alire
Main Book: “Concurrent and Real-Time Programming in Ada” by Alan Burns and Andy Wellings

What you’ll build: A command-line simulation of a four-way traffic intersection. Each direction will be managed by its own concurrent task. A central controller will coordinate the tasks to ensure that lights change in a safe sequence and conflicting directions are never green at the same time.

Why it teaches Ada: This project is the ideal introduction to Ada’s best-in-class concurrency model. You will build a complex, interacting system not with mutexes and condition variables, but with high-level language constructs. It will show you how to reason about concurrent systems safely.

Core challenges you’ll face:

Modeling a traffic light as a task → maps to using task type to create multiple, identical concurrent units
Communicating between tasks → maps to designing entry points on a task to receive signals
Ensuring safe state changes → maps to using a central controller task or a protected object to act as a mutex
Handling timing → maps to using the delay statement to control the simulation speed

Key Concepts:

Tasks and Task Types: “Programming in Ada 2012” Ch. 18 - John Barnes
Rendezvous (entry, accept): The primary mechanism for direct task-to-task communication.
Protected Objects: A simpler, more efficient mechanism for shared data than a full task.

Difficulty: Intermediate Time estimate: 1-2 weeks Prerequisites: Project 1.

Real world outcome: A running console application that prints the state of the intersection over time, proving it never enters an unsafe state.

Time: 0s | North/South: GREEN  | East/West: RED
Time: 1s | North/South: GREEN  | East/West: RED
...
Time: 10s| North/South: YELLOW | East/West: RED
Time: 12s| North/South: RED    | East/West: RED
Time: 13s| North/South: RED    | East/West: GREEN
...

Implementation Hints:

Define an enumeration for the light colors: type Light_Color is (Red, Yellow, Green);.
Define a task type Traffic_Light that represents one direction. This task might have an entry Set_Color(New_Color : in Light_Color);. Inside its body, it would loop forever, printing its current color.
Create a central Controller task. This task will contain the main state machine logic.
In the Controller’s body, you will have a loop that implements the traffic logic:
- Call North_South_Light.Set_Color(Green);.
- delay 10.0;
- Call North_South_Light.Set_Color(Yellow);.
- delay 2.0;
- … and so on.
An alternative and often better design is to use a protected object to hold the state of the lights. The tasks for each light would call entries on the protected object to request a state change, and the protected object would contain the logic to grant or deny the change, ensuring mutual exclusion automatically.

Learning milestones:

You have multiple tasks running and printing their states concurrently → You understand basic tasking.
The lights change state in a coordinated sequence → You understand task communication via entries.
The simulation runs predictably and without race conditions → You appreciate the safety of Ada’s concurrency model.
You can add a “pedestrian button” feature that interrupts the normal cycle → You can handle more complex, asynchronous interactions.

Project 3: Contract-Based Bank Account

File: LEARN_ADA-DEEP_DIVE.md
Main Programming Language: Ada
Alternative Programming Languages: Eiffel
Coolness Level: Level 3: Genuinely Clever
Business Potential: 1. The “Resume Gold”
Difficulty: Level 2: Intermediate
Knowledge Area: Design by Contract / Exceptions / Verification
Software or Tool: GNAT (with assertion checks enabled)
Main Book: “High-Integrity Software: The SPARK Approach to Safety and Security” by John McCormick and Peter C. Chapin

What you’ll build: A package for managing a bank account, with strict contracts (Pre and Post conditions) on all operations. For example, Withdraw will have a precondition that the amount is positive and a postcondition that the new balance is correct. Attempting to withdraw too much will raise a custom exception.

Why it teaches Ada: This project introduces the “Design by Contract” philosophy that underpins high-integrity Ada development. It shifts error handling from defensive if/then checks inside your code to explicit, formal contracts on the API boundary. This makes code clearer, more robust, and even formally provable.

Core challenges you’ll face:

Defining a private account type → maps to encapsulation using private types in a package spec
Writing Pre and Post conditions → maps to learning the contract syntax and logic
Defining and raising custom exceptions → maps to Insufficient_Funds : exception; and the raise statement
Compiling and running with assertions enabled → maps to using the -gnata compiler flag to turn your contracts into runtime checks

Key Concepts:

Design by Contract: “Programming in Ada 2012” Ch. 11 - John Barnes
Private Types: Hiding implementation details.
Exception Handling: “Programming in Ada 2012” Ch. 10 - John Barnes

Difficulty: Intermediate Time estimate: Weekend Prerequisites: Project 1.

Real world outcome: A robust bank account module that is impossible to misuse without triggering a contract violation or an exception.

-- In your demo procedure
My_Account : Account;
Initialize (My_Account, Balance => 100.0);

Deposit (My_Account, Amount => 50.0); -- OK
Withdraw (My_Account, Amount => 20.0); -- OK
Put_Line ("Balance is: " & Get_Balance(My_Account)'Image); -- Balance is: 130.0

begin
   Withdraw (My_Account, Amount => -10.0); -- Fails Precondition! Raises Assert_Error.
exception
   when Ada.Assertions.Assert_Failure =>
      Put_Line ("Error: Cannot withdraw a negative amount.");
end;

begin
   Withdraw (My_Account, Amount => 200.0); -- Fails business logic.
exception
   when Insufficient_Funds =>
      Put_Line ("Error: Not enough money in account.");
end;

Implementation Hints:

In your package spec (.ads), define the account type as private:

package Bank is
   type Account is private;
   procedure Withdraw (A : in out Account; Amount : in Money) with
      Pre => Amount > 0.0,
      Post => Get_Balance(A) = Get_Balance(A)'Old - Amount;
   -- ... other procedures ...
private
   type Account is record
      Balance : Money := 0.0;
   end record;
end Bank;

In the body (.adb), implement Withdraw. Inside, you’ll have an if statement. If Amount > A.Balance, you’ll raise Insufficient_Funds;. Otherwise, you’ll perform the subtraction.
The magic is that the Pre and Post conditions are checked outside your implementation logic. If a caller violates the precondition, the program stops before your code even runs. If your implementation has a bug and fails to meet the postcondition, the program stops after it runs, flagging your error.

Learning milestones:

Your procedures have working pre- and post-conditions → You understand contract syntax.
Violating a precondition raises an Assert_Failure → You see contracts as runtime checks.
Your code correctly raises a custom exception for business logic failures → You can separate contract violations from expected errors.
You start specifying contracts for all your new procedures by default → You are programming with a high-integrity mindset.

Project 4: SPARK-Verified Bounded Stack

File: LEARN_ADA_DEEP_DIVE.md
Main Programming Language: SPARK (a subset of Ada)
Alternative Programming Languages: N/A
Coolness Level: Level 5: Pure Magic (Super Cool)
Business Potential: 1. The “Resume Gold”
Difficulty: Level 4: Expert
Knowledge Area: Formal Verification / Provable Software
Software or Tool: GNAT, SPARK, gnatprove
Main Book: “Building High Integrity Applications with SPARK” by Philip Daian et al.

What you’ll build: A generic, fixed-size stack data structure. You will write it in the SPARK language (a formally analyzable subset of Ada). You will then use the gnatprove tool to mathematically prove that your implementation is free of all runtime errors, such as index-out-of-bounds, integer overflow, and uninitialized variable access.

Why it teaches Ada: This project takes you to the apex of Ada’s philosophy. You are not just writing safe code; you are writing provably correct code. This introduces you to formal verification, a technique used for the most critical software on Earth. It’s a completely different way of thinking about programming, where you work with the verifier to prove your code’s correctness.

Core challenges you’ll face:

Writing code within the SPARK subset → maps to avoiding pointers and other features that are hard to analyze
Adding assertions and loop invariants → maps to giving hints to the formal verification engine
Running gnatprove and interpreting its output → maps to learning to “talk” to the prover and fix the issues it finds
Proving the absence of runtime errors → maps to the ultimate goal of formal verification

Key Concepts:

SPARK Language: A subset of Ada designed for formal proof.
Flow Analysis: How gnatprove tracks data and variable initialization.
Proof-Driven Development: Writing code in a way that makes it easy for the prover to analyze.

Difficulty: Expert Time estimate: 2-3 weeks Prerequisites: Project 3, a solid grasp of Ada basics.

Real world outcome: A stack implementation and a report from the gnatprove tool certifying its correctness.

$ gnatprove -P default.gpr -j0 --level=4
Phase 1 of 2: flow analysis ...
Phase 2 of 2: proof of all checks ...
Summary of proof results:
  Stack.ads:15:14: info: initial condition proved
  Stack.adb:23:17: info: loop invariant proved
  Stack.adb:28:13: info: check proved (range check)
  ...
Analysis results:
  Flow analysis passed.
  Proof results:
    For package Stack:
      All checks proved.

This output means you have mathematically guaranteed your code is free of an entire class of devastating bugs.

Implementation Hints:

Your package will be generic: generic type Element_Type is private; package Stacks is ....
The stack itself will be a record containing an array and a Top index.
On the Push procedure, you will add a Pre condition: Pre => not Is_Full(Stack).
On the Pop procedure, you’ll add a Pre condition: Pre => not Is_Empty(Stack).
When you first run gnatprove, it will likely fail and ask for more information. For example, it might not be able to prove that your Top index always stays within the array bounds. You’ll need to add an assertion or a type invariant like Type_Invariant => Stack.Top in 0 .. Capacity.
The process is iterative: run gnatprove, read the error, add a contract or assertion to help the prover, and repeat until everything is green.

Learning milestones:

Your code is accepted by the SPARK parser → You can write in the required language subset.
gnatprove completes its flow analysis successfully → You have no uninitialized variables or data flow issues.
You successfully prove your first check (e.g., an index bound) → You understand how to interact with the prover.
All checks are proved for the entire module → You have written a piece of formally verified, high-integrity software.

Project 5: Text-Based Adventure Game

File: LEARN_ADA_DEEP_DIVE.md
Main Programming Language: Ada
Alternative Programming Languages: C++, Python
Coolness Level: Level 3: Genuinely Clever
Business Potential: 1. The “Resume Gold”
Difficulty: Level 2: Intermediate
Knowledge Area: Program Architecture / Packages / Data Structures
Software or Tool: GNAT, Alire
Main Book: “Ada Distilled” by Richard Riehle

What you’ll build: A classic text-based adventure game (like Zork). The player can move between rooms, pick up items, and interact with the world by typing commands like “go north”, “take lamp”, etc.

Why it teaches Ada: This is a fun and motivating project for learning how to structure a larger application in Ada. The separation of the game world, the command parser, and the player state fits perfectly with Ada’s package-based architecture. You’ll get extensive practice with strings, containers, and defining your own types for game objects.

Core challenges you’ll face:

Modeling the game world → maps to using records for rooms and items, and arrays or maps to connect them
Parsing player input → maps to Ada’s string handling and I/O libraries
Managing player and game state → maps to designing packages to hold the state and expose safe modification procedures
Structuring the whole application → maps to using packages to create clean separation between the game engine, data, and parser

Key Concepts:

Ada.Strings.Unbounded: The standard library for handling dynamic strings.
Ada.Containers: The Ada equivalent of the C++ STL, providing vectors, maps, etc.
Record Types: Ada’s version of structs.
Package-based design: Structuring a program into logical, encapsulated units.

Difficulty: Intermediate Time estimate: 2-3 weeks Prerequisites: Basic Ada syntax.

Real world outcome: A playable game.

You are in a dusty hall. There is a door to the north and a passage to the east.
A small brass lamp lies on the floor.
> take lamp
You pick up the lamp.

> go north
The door is locked.

> inventory
You are carrying:
  - a brass lamp

Implementation Hints:

World Package: Create a Game_World package. Define types for Room and Item. A Room record could contain its description and an array of exits.
State Package: Create a Game_State package to hold the player’s current location and inventory (Ada.Containers.Vectors would work well for the inventory).
Parser Package: Create a Parser package with a procedure that reads a line of input, splits it into a verb (“go”) and a noun (“north”), and returns a command record.
Main Loop: Your main procedure will loop:
- Print the description of the current room.
- Call the parser to get a command.
- Use a case statement on the command’s verb to execute the action (e.g., change player’s location, add item to inventory).

This clean separation is very idiomatic Ada. You could swap out the entire Game_World with a different map without touching the parser or main loop.

Learning milestones:

You can move between rooms → You have a working game loop and state management.
You can pick up and drop items → You are manipulating container data structures.
Your code is cleanly separated into packages → You are thinking about software architecture in the Ada way.
The game is fun to play → You have successfully built a complete, non-trivial application.

Summary