AIUI, SPARK does not use a Rust-like borrow checker: it's based on formal verification which is a lot more difficult to program for, i.e. not really feasible ex

AIUI, SPARK does not use a Rust-like borrow checker: it's based on formal verification which is a lot more difficult to program for, i.e. not really feasible except for smaller programs. This seems to be in sharp contrast to Rust - the safe subset of Rust enforces a set of rules that can actually scale up to larger programs while still preserving safety.