У AdaCore есть ещё один любопытный вариант "указателей с гарантией". К слову, тренировки с указателями для SPARK там были ещё до появления Rust в массы -- в рамках экспериментального языка ParaSail (Parallel Specification and Implementation Language):
https://adacore.github.io/ParaSail/Это Ada-подобный язык с гарантиями в стиле высоких уровней SPARK (без exception, без runtime-проверок (ака выход за границы массива, переполнения и т.п.) -- статические доказательства). Владеющих указателей в языке нет, но они замаскированы в виде опциональных типов -- любой тип может быть объявлен с модификатором optional, и его значение тогда может принимать в том числе и null (как в SQL, например). Для облегчения работы с такими типами кроме копирования введены стандартные операции перемещения (move как оператор "<==") и обмена (swap: "<=>"). В SPARK семантика опциональных типов переехала на обычные указатели с привычной операцией копирования (которая иногда работает как перемещение, при необходимости источник для копирования может быть установлен в null).
А также в язык введены временные ссылки как переменные, объявляемые через "ref" вместо "var". Пример:
Код:
func Expand (var HT : Hash_Table) is
// Double the size of the Hash_Table backbone
var Old_Backbone <== HT.Backbone // Move old backbone to temp
const New_Len := |Old_Backbone| * 2
// Create backbone with double the number of buckets
HT.Backbone := Create(New_Len, null)
for each Old_Bucket of Old_Backbone loop
for Old_Elem => Old_Bucket then Old_Elem.Next while Old_Elem not null loop
const New_Hash := Hash(Key_Of(Old_Elem.Entry)) mod New_Len
ref New_Bucket => HT.Backbone[New_Hash + 1]
// Insert at front, using ``move''s to create new node.
New_Bucket := Node::(Entry <== Old_Elem.Entry, Next <== New_Bucket)
end loop
end loop
end func Expand
Выше переменная "ref New_Bucket", инициализируемая через "=>", является ака временным (не владеющим) указателем, принимающим такие же права (чтение/запись) как у исходного объекта (и разделяет с ним доступ с контролем уникальности прав на изменение). Аргументы для for-циклов также являются ссылками. Ссылки могут быть только как локальные объекты, они не являются частью так называемого "object declaration" -- не могут быть в составе записей (структур). Параметры процедур также могут быть ссылками, в том числе и в качестве возвращаемых, но только на объект, содержащийся в аргументах процедуры в виде ссылки, или его часть. Например, через ссылки работают операции индексации, которые можно определить для своих типов:
Код:
interface PSL::Containers::Hash_Table<KV_Type is Keyed<>> is
...
// объявление оператора "[...]", с предусловием
op "indexing"(ref T: Hash_Table; Key: KV_Type::Key_Type){Key in T} -> ref KV_Type
...
end interface PSL::Containers::Hash_Table
В общем, у AdaCore есть наработки для временных ссылок (дающих некоторое удобство и скорость/экономию ресурсов) и унификации произвольного доступа (обобщённая подконтрольная индексация). С учётом того, что фишки ParaSail сейчас перелазят в новый стандарт Ada (методики параллельного программирования, вариации циклов, в том числе параллельных, те же владеющие указатели и пр.), можно предположить, что и ссылки с индексацией каким-то образом подтянутся в Ada/SPARK. Очень достойный симбиоз вырисовывается...