How Ada and Rust Think About Safety — Comparing Types, Overflow, Ownership, Data Races, and Formal Verification by Running Them

Ada and Rust are both often introduced as “safe languages.” But what each treats as an error, and where it stops that error, is not the same. Rust focuses on stopping memory misuse and data races at compile time through its ownership and type rules. Ada has you write value ranges into types and, by default, stops out-of-range values at run time. And with SPARK, a subset of Ada, you can prove before running the program that no run-time errors will occur.

This article compares the two from the following six angles:

• How value ranges are expressed in types
• How integer overflow is handled
• How memory misuse is stopped
• How data races are stopped
• How the mechanisms for turning checks off are fenced in
• How formal verification is done

For each angle, I wrote small programs in both Ada and Rust and include the results of actually compiling, running, and proving them. This article does not decide which language is better. The goal is that, by the end, you can judge which way of protecting a program fits your requirements.

An overview of Ada is in “The Appeal of the Ada Language”, and the basics of SPARK are in “Introduction to Formal Verification with SPARK”.

What we compare and the environment used

First, a diagram of where each one stops errors. Rust checks types and ownership inside the compiler; Ada has, in addition to the compiler’s checks, run-time checks as rules of the language. SPARK proofs are done by GNATprove in a stage separate from compilation.

flowchart TB
        accTitle: Where Ada and Rust stop errors
        accDescr: Shows that Rust checks types and ownership at compile time, Ada has compile-time type checks and run-time range checks, and SPARK stops errors before execution through proofs by GNATprove.
        SRC["Source code"] --> C["Compile-time checks"]
        C -->|"Rust"| R1["Types, ownership, borrowing, Send/Sync"]
        C -->|"Ada"| A1["Types, accessibility rules"]
        SRC --> P["Proof by GNATprove"]
        P --> S1["SPARK: absence of run-time errors and races"]
        R1 --> RUN["Run-time checks"]
        A1 --> RUN
        RUN -->|"Rust"| R2["Panic"]
        RUN -->|"Ada"| A2["Constraint_Error and others"]

Figure 1: Rust’s emphasis is on compile-time checks, Ada has run-time checks as rules, and SPARK adds proof before execution.

The environment was as follows. Everything ran on Ubuntu Linux (x86_64).

In the diagram a solid line marks a relation that always holds and a dashed line marks a conditional one (the conditions are given per relation on the detail page). The full list of relations (37 in total, with evidence and certainty) and the definitions of the main concepts are collected on the knowledge map detail page (in Japanese). Data: JSON-LD / Turtle

Expressing value ranges in types: Ada’s ranged types and Rust’s newtype

Ada: derived types and ranged subtypes

In Ada, types declared with different names are different types even if their structure is the same. In the following program, Meters and Feet are both made from Float, but passing a Feet value as a Meters argument is a compile error.

with Ada.Text_IO; use Ada.Text_IO;

procedure Units is
   type Meters is new Float;
   type Feet   is new Float;

   procedure Climb (Height : Meters) is
   begin
      Put_Line ("climb" & Meters'Image (Height));
   end Climb;

   H : constant Feet := 10.0;
begin
   Climb (H);
end Units;

units.adb:14:11: error: expected type "Meters" defined at line 4
units.adb:14:11: error: found type "Feet" defined at line 5

flowchart TB
        accTitle: The difference between Ada derived types and subtypes
        accDescr: Shows that the derived types Meters and Feet made from Float are distinct types and mixing them is a compile error, while the Integer subtype Percent stays the same type as Integer and has its range checked on assignment.
        F["Float"] -->|"type … is new"| M["Meters"]
        F -->|"type … is new"| FT["Feet"]
        M -.->|"Pass one for the other"| E1["Compile error"]
        FT -.-> E1
        I["Integer"] -->|"subtype … range"| P["Percent (0 to 100)"]
        P --> C1["Assignable without conversion"]
        C1 --> C2["Range checked on assignment"]

Figure 2: A derived type becomes a different type; a subtype stays the original type and only adds a range check.

A value range can be written into a type with subtype. The following Percent is a subtype of Integer that allows only 0 to 100. Because it is the same type as Integer, you can assign to it without conversion, and only the range is checked on assignment. This program is used again in later sections, so it also includes lines for a mod type and for overflow.

with Ada.Command_Line; use Ada.Command_Line;
with Ada.Text_IO;      use Ada.Text_IO;

procedure Checks_Demo is
   type Byte is mod 256;                      --  A type declared to wrap around
   subtype Percent is Integer range 0 .. 100; --  A type that allows only 0 to 100

   N : constant Integer := Integer'Value (Argument (1));
   B : Byte := Byte (N mod 256);
   P : Percent;
begin
   B := B + 1;
   Put_Line ("Byte:    " & Byte'Image (B));
   Put_Line ("N + 1:   " & Integer'Image (N + 1));
   P := N;
   Put_Line ("Percent: " & Percent'Image (P));
end Checks_Demo;

I built it with gnatmake checks_demo.adb and ran it with different arguments.

$ ./checks_demo 50
Byte:     51
N + 1:    51
Percent:  50
$ ./checks_demo 255
Byte:     0
N + 1:    256

raised CONSTRAINT_ERROR : checks_demo.adb:15 range check failed

On line 15, which assigns 255 to Percent, Constraint_Error was raised and the program stopped. You write the range once in the type declaration, and it is checked on every assignment to a variable of that type.

Rust: newtypes and constructor functions

In Rust, the newtype pattern, which wraps an existing type in a one-field struct, uses types to prevent mixing up units. The Rust Programming Language (hereafter, the Rust Book) explains that a program that passes a Meters or a bare u32 to a function taking Millimeters will not compile¹.

struct Meters(f64);
struct Feet(f64);

fn climb(height: Meters) {
    println!("climb {}", height.0);
}

fn main() {
    let h = Feet(10.0);
    climb(h);
}

error[E0308]: mismatched types
  --> units.rs:10:11
   |
10 |     climb(h);
   |     ----- ^ expected `Meters`, found `Feet`

On the other hand, Rust types have no syntax for writing a value range like Ada’s range. To enforce a range, you make the struct’s field impossible to construct from outside and provide a constructor function that checks it.

use std::env;

#[derive(Debug, Clone, Copy)]
struct Percent(u8);

impl Percent {
    fn new(value: i32) -> Option<Percent> {
        if (0..=100).contains(&value) {
            Some(Percent(value as u8))
        } else {
            None
        }
    }
}

fn main() {
    let n: i32 = env::args().nth(1).unwrap().parse().unwrap();
    println!("{:?}", Percent::new(n));
}

$ ./percent 42
Some(Percent(42))
$ ./percent 120
None

Instead of stopping with an exception when the value is out of range, it returns an Option and lets the caller handle it. Because this example fits in one file, main can construct Percent(…) directly, but if you move the type into a module and make the field private, code outside has no choice but to go through Percent::new. Note that a Rust type alias (type Kilometers = i32;) does not create a separate type, and the compiler does not treat mixing them as an error¹. Ada’s subtype can also be mixed with its original type, but the range check comes along with it.

flowchart TB
        accTitle: Where out-of-range values are stopped
        accDescr: Shows that Ada checks the range on every assignment to a subtype and raises Constraint_Error, while Rust checks the range in a constructor function and returns None when it is out of range.
        V["An out-of-range value"] --> A["Ada: assign to a subtype"]
        V --> R["Rust: pass to a constructor"]
        A --> A2["Range check on every assignment"]
        A2 --> A3["Constraint_Error"]
        R --> R2["Checked inside the constructor"]
        R2 --> R3["Returns None"]

Figure 3: Ada checks the range written in the type declaration on every assignment; Rust checks in a constructor and returns the result as a value.

Integer overflow: exception, panic, or wraparound

Ada: Constraint_Error for signed integers, wraparound for mod types

In the Ada language specification, the predefined operations on integer types either return the mathematically correct result or raise Constraint_Error². When the result of an operation on a signed integer type exceeds the type’s range, it raises Constraint_Error, and a modular type declared with mod wraps around modulo its modulus³. GNAT enables overflow checks by default⁴.

Passing Integer'Last (2147483647) to the earlier checks_demo stopped at N + 1 on line 14. In the same run, the mod 256 Byte wrapped 255 + 1 around to 0.

$ ./checks_demo 2147483647
Byte:     0

raised CONSTRAINT_ERROR : checks_demo.adb:14 overflow check failed

Values that may wrap around are distinguished as mod types at the point of the type declaration. Even with the same +, the type decides whether it wraps around or stops.

Rust: the result depends on build settings

The Rust language specification treats overflow as an error and distinguishes it from intended wraparound. In builds where debug_assert! is enabled (such as unoptimized builds), it requires checks that panic on overflow. For other builds, it leaves it to the implementation whether to panic or silently wrap around. When it wraps around, the result is determined by two’s complement rules⁵. Cargo’s defaults are overflow-checks = true for the dev profile and overflow-checks = false for the release profile⁶.

I checked with the following program. checked_add, wrapping_add, and saturating_add are methods that let the caller choose what happens on overflow.

use std::env;

fn main() {
    // The value is read from a run-time argument, so it is not a constant at compile time
    let x: u8 = env::args().nth(1).unwrap().parse().unwrap();
    println!("checked_add:    {:?}", x.checked_add(1));
    println!("wrapping_add:   {}", x.wrapping_add(1));
    println!("saturating_add: {}", x.saturating_add(1));
    let y = x + 1;
    println!("x + 1 = {}", y);
}

With cargo run (the dev profile), it panicked on the x + 1 line. The exit code was 101.

$ cargo run -q -- 255
checked_add:    None
wrapping_add:   0
saturating_add: 255

thread 'main' (10929) panicked at src/main.rs:9:13:
attempt to add with overflow
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

With cargo run --release, the same expression wrapped around to 0 and processing continued. The exit code was 0.

$ cargo run -q --release -- 255
checked_add:    None
wrapping_add:   0
saturating_add: 255
x + 1 = 0

Adding the following setting to Cargo.toml made the release profile panic just like dev. When you use rustc directly, rustc -O -C overflow-checks=on gives the same result.

[profile.release]
overflow-checks = true

flowchart TB
        accTitle: How the handling of integer overflow branches
        accDescr: In Ada, signed integer types raise Constraint_Error and mod types wrap around. In Rust, it panics if overflow-checks is enabled, and with the local rustc it wrapped around when disabled.
        O["Integer overflow"] --> A["Ada: decided by the type"]
        O --> R["Rust: decided by build settings"]
        A -->|"Signed integer type"| A1["Constraint_Error"]
        A -->|"mod type"| A2["Wraps around modulo"]
        R -->|"overflow-checks enabled"| R1["Panic"]
        R -->|"overflow-checks disabled"| R2["Wraps around in two's complement"]

Figure 4: In Ada the type declaration, and in Rust the build settings, decide the result of an overflow.

What happens when checks are turned off

Both let you turn checks off. What the result means differs.

In Ada, you can turn checks off with pragma Suppress or GNAT’s -gnatp (which suppresses all checks)⁴. The language specification says that when such an error occurs with its check suppressed, the execution is “erroneous”⁷. Rebuilding with gnatmake -gnatp checks_demo.adb gave the following result.

$ ./checks_demo 2147483647
Byte:     0
N + 1:   -2147483648
Percent:  2147483647

N + 1 became negative, and Percent, which should only allow 0 to 100, holds 2147483647. These values are only what I observed locally; for erroneous execution, the language specification does not define the result.

Wraparound in a Rust release build has its result determined by two’s complement rules, as seen above. The language specification treats this as an error but classifies it as one of the “behaviors not considered unsafe”⁵. In Ada, keeping the checks is the default, and if you turn them off the result is not guaranteed. In Rust, turning the checks off is the default for release builds, and even with them off the result is defined. The two are opposite both in where the default sits and in what turning the checks off means.

flowchart TB
        accTitle: How results are treated when checks are turned off
        accDescr: Shows that in Ada, when checks are suppressed with -gnatp or similar and an error occurs, the execution is erroneous and the result is undefined, whereas in Rust with overflow-checks disabled the result is the value wrapped around in two's complement.
        A["Ada: checks suppressed with -gnatp"] --> A1["Overflow or out of range"]
        A1 --> A2["Erroneous execution"]
        A2 --> A3["The specification does not define the result"]
        R["Rust: overflow-checks disabled"] --> R1["Overflow"]
        R1 --> R2["Wraps around in two's complement"]
        R2 --> R3["The result is defined"]

Figure 5: With checks turned off, the result is undefined in Ada and is the wrapped-around value in Rust.

Memory safety: ownership and access types

Rust: ownership and the borrow checker

The Rust Book sums up the ownership rules in three points: each value has an owner, there can be only one owner at a time, and when the owner goes out of scope the value is dropped. The compiler checks these rules, and code that violates them does not compile⁸. Under the borrowing rules, at any given time you can have either one mutable reference or any number of immutable references, and references must always be valid⁹. The borrow checker compares scopes to decide whether borrows are valid¹⁰.

Using a variable after its ownership has been moved is a compile error.

fn main() {
    let a = String::from("hello");
    let b = a;
    println!("{} {}", a, b);
}

error[E0382]: borrow of moved value: `a`
 --> moved.rs:4:23
  |
2 |     let a = String::from("hello");
  |         - move occurs because `a` has type `String`, which does not implement the `Copy` trait
3 |     let b = a;
  |             - value moved here
4 |     println!("{} {}", a, b);
  |                       ^ value borrowed here after move

flowchart TB
        accTitle: Moving ownership in Rust
        accDescr: Shows that let b = a moves ownership of the String from a to b, that using a after that is a compile error, and that the value is dropped when b goes out of scope.
        A["a owns a String"] -->|"let b = a"| B["b becomes the owner"]
        B --> U["Use a"]
        U --> E["E0382: use after move"]
        B --> D["b goes out of scope"]
        D --> DR["The value is dropped"]

Figure 6: Assignment moves ownership, and using the source of the move is a compile error.

The borrow checker also stops code that keeps a reference to a variable that has gone out of scope.

fn main() {
    let r;
    {
        let s = String::from("hello");
        r = &s;
    }
    println!("{}", r);
}

error[E0597]: `s` does not live long enough
 --> dangling.rs:5:13
  |
4 |         let s = String::from("hello");
  |             - binding `s` declared here
5 |         r = &s;
  |             ^^ borrowed value does not live long enough
6 |     }
  |     - `s` dropped here while still borrowed
7 |     println!("{}", r);
  |                    - borrow later used here

Ada: access types and accessibility rules

Pointers in Ada are called access types. The language specification states that the accessibility rules prevent dangling references¹¹. Writing the same shape as the second Rust example above in Ada produced a compile error.

with Ada.Text_IO; use Ada.Text_IO;

procedure Dangling is
   type Int_Ptr is access all Integer;
   P : Int_Ptr;
begin
   declare
      X : aliased Integer := 1;
   begin
      P := X'Access;
   end;
   Put_Line (Integer'Image (P.all));
end Dangling;

dangling.adb:10:12: error: non-local pointer cannot point to local object

However, what the accessibility rules look at is the relationship between the pointer’s type and the lifetime of what it points to. They do not stop use after memory allocated with new has been freed with Ada.Unchecked_Deallocation.

with Ada.Text_IO; use Ada.Text_IO;
with Ada.Unchecked_Deallocation;

procedure Use_After_Free is
   type Int_Ptr is access Integer;
   procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr);

   X : Int_Ptr := new Integer'(1);
   Y : constant Int_Ptr := X;   --  A second pointer to the same memory
begin
   Free (X);                    --  X becomes null, but Y is unchanged
   Put_Line (Boolean'Image (X = null));
   Put_Line (Integer'Image (Y.all));   --  Read the freed memory
end Use_After_Free;

Even with gnatmake -gnatwa (which enables almost all warnings), it built without errors or warnings, and running it gave the following. The second line was a different value on every run.

TRUE
 1610868145

In the language specification, X becomes null after Free(X). On the other hand, an execution that dereferences a pointer to freed memory (a dangling reference) is erroneous¹². Free sets only the X you passed to null and does not touch Y, which points to the same memory.

flowchart TB
        accTitle: Pointer state before and after Free
        accDescr: Shows that when Free(X) is called while X and Y point to the same memory, X becomes null and the memory is freed, but Y remains pointing to the freed memory.
        S["X and Y point to the same memory"] --> F["Call Free(X)"]
        F --> XN["X becomes null"]
        F --> HF["The memory is freed"]
        HF --> YD["Y still points to the freed memory"]

Figure 7: Free sets only the pointer you pass to null; other pointers to the same memory remain.

flowchart TB
        accTitle: Where pointer misuse is stopped
        accDescr: Rust stops use after a move of ownership and references that escape their scope at compile time. Ada stops pointers to local variables from escaping at compile time but does not stop use after free, which SPARK's ownership policy stops at the proof stage.
        E["Pointer misuse"] --> R["The Rust compiler"]
        E --> A["The Ada compiler"]
        R --> R1["Rejects use after move"]
        R --> R2["Rejects references that outlive their target"]
        A --> A1["Rejects letting a local variable escape"]
        A --> A2["Use after free gets through"]
        A2 -.-> S["SPARK's ownership policy"]

Figure 8: Rust stops misuse with its ownership and borrowing rules and Ada with its accessibility rules; the use after free that Ada does not stop is handled by SPARK.

SPARK: an ownership policy modeled on Rust

The SPARK User’s Guide says that “Like Rust, SPARK enforces an ownership policy for memory.” When you assign a variable of an access type, ownership moves to the left-hand side, and the right-hand side loses the right to access that memory. There is also observing, which shares read-only access, and borrowing, which hands over ownership temporarily¹³.

The following code moves ownership to Y and then writes through X.

with Ada.Unchecked_Deallocation;

procedure Move_Demo with SPARK_Mode is
   type Int_Ptr is access Integer;
   procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr);

   X : Int_Ptr := new Integer'(1);
   Y : Int_Ptr;
begin
   Y := X;        --  Ownership moves from X to Y
   X.all := 2;    --  Write through X after the move
   Free (Y);
end Move_Demo;

GNAT compiled this code as is, and running it ended without anything happening. Run through GNATprove, it reports that X, moved on line 10, is used on line 11.

move_demo.adb:11:06: error: dereference from "X" is not writable
   11 |   X.all := 2;    --  Write through X after the move
      |   ~~^~~
  object was moved at line 10 [E0010]
   10 |   Y := X;        --  Ownership moves from X to Y
      |        ^ here

SPARK also checks for memory leaks. According to the User’s Guide, GNATprove checks on every assignment that the left-hand side does not leak memory, and on every declaration that it does not leak memory at the end of its lifetime¹³. Changing line 11 to Y.all := 2; and removing Free (Y); produced the following report.

move_demo.adb:8:04: medium: resource or memory leak might occur at end of scope

Putting Free (Y); back proved that there are no leaks and that all pointer dereference checks pass.

move_demo.adb:7:04: info: absence of resource or memory leak at end of scope proved
move_demo.adb:8:04: info: initialization of "Y" proved
move_demo.adb:8:04: info: absence of resource or memory leak at end of scope proved
move_demo.adb:10:06: info: absence of resource or memory leak proved
move_demo.adb:11:06: info: pointer dereference check proved

Here there is one difference from Rust. The Rust language specification lists leaks of memory and other resources among the “behaviors not considered unsafe”⁵. In other words, safe Rust code does not go as far as promising that there are no leaks. SPARK makes leaks a subject of proof.

flowchart TB
        accTitle: What GNATprove looks at under SPARK's ownership policy
        accDescr: Shows that assigning an access type moves ownership, that GNATprove makes use after the move an error, and that it checks for memory leaks at the end of lifetimes and on assignment.
        AS["Access type assignment Y := X"] --> MV["Ownership moves to Y"]
        MV --> U["Use X"]
        U --> E1["Error: use after move"]
        MV --> L["Y's lifetime ends"]
        L -->|"Without Free"| E2["Reports a possible leak"]
        L -->|"With Free"| OK["Proves there is no leak"]

Figure 9: GNATprove makes use after a move an error and also checks that memory has been freed by the end of its lifetime.

Data races: Send/Sync and protected objects

Rust: the borrowing rules and Send/Sync stop them at compile time

The Rust Book explains that the rules for references prevent data races at compile time⁹. The following code, in which four threads keep adding to the same variable, does not compile because the mutable borrows overlap.

use std::thread;

fn main() {
    let mut count = 0;
    thread::scope(|s| {
        for _ in 0..4 {
            s.spawn(|| {
                for _ in 0..100_000 {
                    count += 1;
                }
            });
        }
    });
    println!("count = {}", count);
}

error[E0499]: cannot borrow `count` as mutable more than once at a time
 --> race.rs:7:21

Whether a type can cross threads is expressed by two marker traits, Send and Sync. Send indicates that ownership of values of that type can be transferred between threads, and Sync indicates that it is safe for the type to be referenced from multiple threads. Rc<T>, which updates its reference count without synchronization, does not implement Send¹⁴.

use std::rc::Rc;
use std::thread;

fn main() {
    let shared = Rc::new(5);
    let handle = thread::spawn(move || {
        println!("{}", shared);
    });
    handle.join().unwrap();
}

error[E0277]: `Rc<i32>` cannot be sent between threads safely
 --> rc_send.rs:6:32
  = help: within `{closure@rc_send.rs:6:32: 6:39}`, the trait `Send` is not implemented for `Rc<i32>`

flowchart TB
        accTitle: Deciding whether a value can be passed to a thread
        accDescr: Shows that if the types of the values held by the closure passed to thread::spawn implement Send, compilation succeeds, and if they do not implement Send, as with Rc, compilation fails with E0277.
        S["Pass a value to thread::spawn"] --> Q["Is the value's type Send?"]
        Q -->|"Implements it"| OK["Compiles"]
        Q -->|"Does not implement it"| NG["Rejected with E0277"]
        NG -.-> EX["Example: Rc's reference count"]

Figure 10: Whether a value passed to a thread is allowed is decided at compile time by whether its type implements Send.

Wrapping the addition in a Mutex made it compile, and the result was 400000.

use std::sync::Mutex;
use std::thread;

fn main() {
    let count = Mutex::new(0);
    thread::scope(|s| {
        for _ in 0..4 {
            s.spawn(|| {
                for _ in 0..100_000 {
                    *count.lock().unwrap() += 1;
                }
            });
        }
    });
    println!("count = {}", count.into_inner().unwrap());
}

count = 400000

Ada: protected objects are available, but code that does not use them also compiles

An Ada protected object lets tasks access shared data only through the operations it exposes, and coordinates that access¹⁵. However, code that updates a shared variable without using a protected object also compiles. The language specification says that an execution in which two unsynchronized actions use the same shared variable in a conflicting way is erroneous¹⁶.

In the following program, four tasks each increment both the unprotected Count and the protected object Counter 100,000 times.

with Ada.Text_IO; use Ada.Text_IO;

procedure Race is
   Count : Integer := 0;

   protected Counter is
      procedure Increment;
      function Value return Integer;
   private
      N : Integer := 0;
   end Counter;

   protected body Counter is
      procedure Increment is
      begin
         N := N + 1;
      end Increment;

      function Value return Integer is (N);
   end Counter;

   task type Worker;
   task body Worker is
   begin
      for I in 1 .. 100_000 loop
         Count := Count + 1;    --  Unprotected shared variable
         Counter.Increment;     --  Through the protected object
      end loop;
   end Worker;
begin
   declare
      Workers : array (1 .. 4) of Worker;
   begin
      null;  --  Wait here for the four tasks to finish
   end;
   Put_Line ("Count   =" & Integer'Image (Count));
   Put_Line ("Counter =" & Integer'Image (Counter.Value));
end Race;

GNAT built it with the default warning settings without any warning. Running it three times on a 4-core machine, the protected object’s value was 400000 every time, and the unprotected variable had a different value every time.

Count   = 345849
Counter = 400000
Count   = 348876
Counter = 400000
Count   = 387245
Counter = 400000

How to use protected objects themselves is covered in detail in “Safe Concurrency with Ada”.

SPARK: GNATprove reports data races

Writing concurrent code in SPARK requires the Ravenscar profile, and GNATprove also supports the Jorvik profile. pragma Partition_Elaboration_Policy (Sequential); is also required so that tasks do not start before elaboration of the whole program is complete. The only things tasks can share are synchronized objects such as protected objects and atomic objects¹⁷. I put pragma Profile (Jorvik); and this pragma in the configuration pragma file and ran GNATprove on a package in which two tasks update an unprotected variable. It produced the following report.

package Shared with SPARK_Mode is
   Count : Integer := 0;

   task type Worker;
   W1, W2 : Worker;
end Shared;

package body Shared with SPARK_Mode is
   task body Worker is
   begin
      loop
         if Count < Integer'Last then
            Count := Count + 1;
         end if;
      end loop;
   end Worker;
end Shared;

shared.ads:5:04: high: possible data race when accessing variable "shared.count"
    5 |   W1, W2 : Worker;
      |   ^~
  task "shared.w1" accesses "shared.count"
  task "shared.w2" accesses "shared.count"

Moving Count into a protected object made this report go away, and the overflow checks and the fact that the tasks do not stop were proved.

flowchart TB
        accTitle: Where unsynchronized access to shared variables is stopped
        accDescr: Rust stops it at compile time with the borrowing rules and Send/Sync. Ada lets it compile and the execution is erroneous. In SPARK, GNATprove reports a possible data race.
        W["Unsynchronized update of a shared variable"] --> R["Rust"]
        W --> A["Ada"]
        W --> S["SPARK"]
        R --> R1["Compile error"]
        A --> A1["Compiles"]
        A1 --> A2["Erroneous execution"]
        S --> S1["GNATprove reports the race"]

Figure 11: Rust stops unsynchronized updates of shared variables at compile time and SPARK at the proof stage; Ada itself does not stop them.

Having no data races does not go as far as meaning there are no errors in the order of operations. The SPARK User’s Guide also gives an example of a race condition remaining in a program with no data races¹⁷. The Rust language specification also lists deadlocks among the “behaviors not considered unsafe”⁵.

The doors for turning checks off: unsafe and Unchecked_

Both languages have mechanisms for turning off the language’s checks. What differs is how their scope is fenced in.

Rust’s unsafe enables only five operations: dereferencing a raw pointer, calling an unsafe function or method, accessing or modifying a mutable static variable, implementing an unsafe trait, and accessing fields of a union. Even inside an unsafe block, the borrow checker and the other checks keep working¹⁸. Dereferencing a raw pointer outside unsafe is a compile error.

fn main() {
    let x = 5;
    let p = &x as *const i32;
    println!("{}", *p);
}

error[E0133]: dereference of raw pointer is unsafe and requires unsafe function or block
 --> rawptr.rs:4:20
  |
4 |     println!("{}", *p);
  |                    ^^ dereference of raw pointer
  |
  = note: raw pointers may be null, dangling or unaligned; they can violate aliasing rules and cause data races: all of these are undefined behavior

As the compiler’s note says, a raw pointer can be null or a dangling reference. If you dereference it inside unsafe, the person who wrote that code guarantees it is correct.

Putting #![forbid(unsafe_code)] at the top of the crate made writing an unsafe block an error.

error: usage of an `unsafe` block
 --> forbid.rs:6:5

The mechanisms for turning checks off in Ada are the ones with Unchecked in their names, Ada.Unchecked_Deallocation, Ada.Unchecked_Conversion, and the 'Unchecked_Access attribute, plus pragma Suppress, which suppresses checks. The language specification says that Unchecked_Access can be used to get around the accessibility rules¹¹. To restrict which units may be used, you can use the language-defined restriction No_Dependence¹⁹. Writing the following produced a compile error on the line that uses Ada.Unchecked_Deallocation.

pragma Restrictions (No_Dependence => Ada.Unchecked_Deallocation);

with Ada.Unchecked_Deallocation;

procedure Restricted is
   type Int_Ptr is access Integer;
   procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr);
   X : Int_Ptr := new Integer'(1);
begin
   Free (X);
end Restricted;

restricted.adb:3:06: error: violation of restriction "No_Dependence => Ada.Unchecked_Deallocation" at line 1

In SPARK, the parts marked SPARK_Mode => Off are excluded from GNATprove’s analysis. Changing the Move_Demo from the previous section to with SPARK_Mode => Off and running GNATprove did not report the use after the move; it only warned that there was no body to analyze.

warning: no checks generated by GNATprove
possible reason: no bodies have been selected for analysis with SPARK_Mode

flowchart TB
        accTitle: How the mechanisms for turning checks off are fenced in
        accDescr: Rust allows only five operations in unsafe blocks and can forbid them with forbid(unsafe_code). Ada turns checks off with units whose names start with Unchecked_ and with pragma Suppress, and can forbid them with the No_Dependence restriction.
        U["Turn off the language's checks"] --> R["Rust: unsafe blocks"]
        U --> A["Ada: Unchecked_ and Suppress"]
        R --> R1["Only five operations allowed"]
        R --> R2["Forbidden with forbid(unsafe_code)"]
        A --> A1["The name shows where it is used"]
        A --> A2["Forbidden with No_Dependence"]

Figure 12: In both, you can find the places where checks are turned off by name, and both have a way to forbid them for a whole project.

In both languages, you can search for the places where checks are turned off by the names unsafe and Unchecked. In code review, read these places first.

Formal verification: SPARK as a language subset, and Rust’s verification tools

SPARK is a subset of Ada: you write contracts (preconditions, postconditions, and so on) in Ada syntax, and GNATprove proves them. The SPARK examples in this article are also Ada code with SPARK_Mode attached. The idea of proof levels is explained in “Introduction to Formal Verification with SPARK”.

Rust has no formal verification built into the language, but there are external tools. The table lists what each tool’s official documentation says. None of these tools were run in this article’s environment.

flowchart TB
        accTitle: Where the formal verification tools stand
        accDescr: SPARK is a subset of Ada and GNATprove proves it. In Rust, external tools such as Kani, Verus, Creusot, and Prusti each verify code in their own way.
        FV["Formal verification"] --> SP["SPARK: a subset of Ada"]
        FV --> RT["Rust: external tools"]
        SP --> GP["GNATprove"]
        RT --> K["Kani: model checking"]
        RT --> V["Verus: proof with Z3"]
        RT --> C["Creusot: translation to Why3"]
        RT --> P["Prusti: built on Viper"]

Figure 13: In SPARK, the language subset and the proof tool come as one; in Rust, external tools each verify code in their own way.

Which way of protecting a program fits your requirements

Here is a summary of the results so far.

When you compare these with your requirements, look at the following points.

• If your main worry is errors in value ranges or units, Ada’s ranged types put a check on every assignment with one line of declaration. If you go as far as SPARK, you can show before running that such violations do not occur.
• If you want the compiler alone to stop memory misuse and data races, Rust’s ownership and Send/Sync do that without additional tools. In Ada itself, the compiler does not stop use after free or unsynchronized sharing, so use SPARK, or restrict the features that may be used with No_Dependence and the like.
• The handling of overflow in release builds has opposite defaults. If you want to keep the checks in Rust, set overflow-checks = true explicitly; if you use -gnatp in Ada, you need to show by some other means that the errors whose checks you turned off do not occur.
• If you require proof, SPARK has both a language subset and a proof tool. In Rust, first check whether the code in question falls within what the tool supports.

flowchart TB
        accTitle: Main concerns and the protection that fits them
        accDescr: Shows that if the main worry is errors in value ranges or units, Ada's ranged types fit; if you want the compiler to stop memory misuse and data races, Rust fits; and if you require proof before execution, SPARK fits.
        Q["Main concern"] --> V["Errors in value ranges or units"]
        Q --> M["Memory misuse and data races"]
        Q --> P["Proof before execution required"]
        V --> V1["Ada's ranged types"]
        M --> M1["Rust's ownership and Send/Sync"]
        P --> P1["SPARK and GNATprove"]

Figure 14: The protection that fits depends on what you mainly want to prevent.

Both languages have tools that make up for their gaps, once you understand how each one protects a program. The concrete steps for proving AI-written code with SPARK are covered in “Proving AI-Written Code with SPARK”, and how Ada handles pointers and deallocation in “Memory Management in Ada”.

Related articles

• The Appeal of the Ada Language
• Introduction to Formal Verification with SPARK
• Safe Concurrency with Ada
• Proving AI-Written Code with SPARK
• Memory Management in Ada
• What’s New in Ada 2022

References

Related Articles

Recent articles sharing the same tags. Deepen your understanding with closely related topics.

Related Topics

These are topic pages close to this theme. Starting from the article, you can go on to related services and other articles.

Services Connected to This Topic

This article leads to the following service pages. Start from the entry point closest to your situation.

Frequently Asked Questions

Questions commonly asked at the time of consultation about the topic of this article.

Which is safer, Ada or Rust?

They cannot be compared in a word. Rust stops memory misuse and data races at compile time with its ownership and borrowing rules. Ada has you write value ranges into types and, by default, stops out-of-range values and overflow at run time. With SPARK, a subset of Ada, you can prove before running the program that no run-time errors occur and that there are no data races. Choose according to the properties you need to guarantee.

What happens to integer overflow in a Rust release build?

In Cargo's release profile, overflow-checks is false by default, so with rustc 1.97.0 on my machine 255u8 + 1 wrapped around to 0 without panicking. The Rust language specification leaves it to the implementation whether to panic or wrap in builds where the debug checks are disabled. Setting overflow-checks = true in Cargo.toml makes release builds panic as well.

Does Ada have anything like Rust's ownership?

Ada itself has accessibility rules, which stop at compile time code in which a pointer to a local variable outlives that variable. However, they do not stop use after deallocation with Unchecked_Deallocation. SPARK has an ownership policy modeled on Rust's, and GNATprove detects use of a pointer after it has been moved, as well as memory leaks.

Does Rust have formal verification like SPARK?

It is not built into the language, but external tools exist. Kani does model checking, Verus does theorem proving with an SMT solver, Creusot does deductive verification using Why3, and Prusti does verification built on Viper. The parts of Rust each tool supports differ, so check each tool's documentation before using it.

Author Profile

Profile page for the article author.

Go Komura

Representative of KomuraSoft LLC

Focused on Windows software development, technical consulting, and bug investigation, with particular strength in projects where existing assets remain and in investigating failures whose cause is hard to see.