Re: Rust's temporal safety for Ada/SPARK

[Robert Eachus <rieachus@comcast.net>]

I'm going to try to avoid getting into a long discussion here.  The part of Rust referenced is similar to Ada without tasking. As Jeffery Carter points out, most of the time Ada scope rules deal with this at compile time.  There are some cases that require run-time checking, and most programmers consider code that needs run-time checking as a bug.  (In SPARK, it is. ;-)

As for concurrency of the type we have been discussing in another thread, it is at a very low level, and should usually only come up in hard real-time code.  If you have time limits in milliseconds or less, just using the Ada thread safe versions of data structures are not well defined enough.  What we are/were discussing was code that is lock free, and where synchronization will cause one CPU core to stall (usually for just much less than a microsecond.) until the data is available, rather than a sleep-state or task switch.