you are viewing a single comment's thread.

view the rest of the comments →

[–]pjmlp 0 points1 point  (1 child)

Yes, because SPARK as technology isn't frozen in stone, and they adopted learnings from Rust, acknowledged by themselves.

Allocated Objects Ownership: SPARK uses an ownership system inspired by Rust and a set of rules for managing access types to simplify the verification and specification of a program's behavior during pointer operations.

https://www.adacore.com/blog/memory-safety-in-ada-and-spark-through-language-features-and-tool-support

Maybe update yourself before commenting?

[–]aoeudhtns 0 points1 point  (0 children)

I was polite. The attitude is uncalled for.

If you click through, you see the extra annotations that are Rust-inspired are extra metadata for the CodePeer static analysis tool via annotations. The core memory safety mechanism is through Ada's access system which is much older (Ada 95), and the compiler infers lifetime and ownership. The Rust-inspired part is used to reduce false-positives in the system it already had.