Hello, I am matklad! I am primarily a Zig/Rust person, but I’ve always been envious of Ada memory management, as it seems to have a super-power, not available in RAII or manually managed languages — returning variable size data without the use of the heap.
Is there some gears-level explanation of how that actually works? the closest I know is On the Ada Secondary Stack, and Allocation in the Real-World , but that doesn’t really look inside the box, only notices its properties.
As a specific example, the following program feels like magic to me:
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
procedure Demo is
-- Define a type for an array of integers
type Int_Array is array (Positive range <>) of Integer;
-- Function to create an array of integers from 1 to N
function Make_Array (N : Positive) return Int_Array is
Result : Int_Array(1 .. N);
begin
for I in Result'Range loop
Result(I) := I;
end loop;
return Result;
end Make_Array;
-- Function to choose between two arrays
function Choose_Array (N1, N2 : Positive; Use_First : Boolean) return Int_Array is
A1 : constant Int_Array := Make_Array(N1);
A2 : constant Int_Array := Make_Array(N2);
begin
if Use_First then
return A1;
else
return A2;
end if;
end Choose_Array;
begin
-- Call Choose_Array from main and print its elements
declare
A : Int_Array := Choose_Array(3, 7, Use_First => False);
begin
for I in A'Range loop
Put(A(I));
Put(" ");
end loop;
New_Line;
end;
end Demo;
We allocate two dynamically-sized arrays, return one of them based on runtime condition, and somehow that all works without heap memory 
? Indistinguishable from magic!
What are the exact runtime data structures and compiler lowerings that make this possible? How does this interact with SPARK?
Thanks!