Re: Rust's temporal safety for Ada/SPARK

[Simon Wright <simon@pushface.org>]

Niklas Holsti <niklas.holsti@tidorum.invalid> writes:

> The container library has made it practical to avoid access types in
> the application code, but then there are other potential run-time
> problems, such as "tampering" with the containers, which require
> run-time checks (and which are to some extent consequences of the use
> of access types within the container library).

The current (GCC 7) containers allow suppression of tampering checks,
see [1], for performance reasons.

I don't believe that the tampering checks are mainly, if at all, the
consequnece of using access types. Suppose you are iterating over an
ordered map and you change the current element so as to alter its sort
key? Or, for that matter, any other element? Suppose you delete the
element you are currently visiting?

[1] http://www.adacore.com/developers/development-log/NF-74-O426-003-gnat/