Re: Implementing Rust's borrow checked pointers

[Optikos <optikos@verizon.net>]

On Tuesday, September 24, 2019 at 7:02:26 AM UTC-5, Lucretia wrote:
> On Tuesday, 24 September 2019 12:23:30 UTC+1, Optikos  wrote:
> 
> > > begin
> > >    A.all ... ; -- raises exception.
> > 
> > No, to be as useful as Rust's borrow checker, instead of raising exception, it needs to be a compile-time
> > error.  The compiler needs to maintain a whole-program directed graph at compile-time, not defer a
> > detection-based localized analysis to run-time.
> 
> Yes, the compiler would raise that exception at compile time. This idea that all exceptions are raised at
> runtime is false and you should check the AARM.

Well, at some vague generalized concept level, I & the AARM agree with your stated principle, but at a narrow technocratic reading of the actual text of the AARM as written you are incorrect.  The proper term-of-art for what you are referring to is “error” not “exception”.  I just checked; each usage throughout the entire AARM of the term “exception” are
1) utilized in the context of run-time •error•
or
2) the English-language general dictionary definition of exclusion from the topic being discussed, such as “There are a few exceptions to this general principle” in the side note in §2.8.

“§1.1.5 Classification of •Errors•

“The language definition classifies errors into several different categories:

“● •Errors• that are required to be detected ••prior to run time•• by every Ada implementation;

“These errors correspond to any violation of a rule given in this International Standard, other than
those listed below. In particular, violation of any rule that uses the terms shall, allowed,
permitted, legal, or illegal belongs to this category. Any program that contains such an error is not
a legal Ada program; …

“The rules are further classified as either •compile•-time rules†, or •post-compilation• rules†, depending
on whether a violation has to be detected at the time a compilation unit is submitted to the
compiler, or may be postponed until the time a compilation unit is incorporated into a partition of
a program.

“● Errors that are required to be detected at run time by the execution of an Ada program;

“The corresponding error situations are associated with the names of the predefined exceptions.
Every Ada compiler is required to generate code that raises the corresponding exception if such an error situation arises during program execution. [If such an •error• situation is certain to arise in
every execution of a construct, then an implementation is •••allowed (although not required)••• to
report this fact at •compilation• time.‡]

“● Bounded errors;

“The language rules define certain kinds of errors that need •not• be detected either •prior to• or
during run time, but if not detected, the range of possible effects shall be bounded. The errors of
this category are called bounded errors. The possible effects of a given bounded error are
specified for each such error, but in any case one possible effect of a bounded error is the raising
of the exception Program_Error.

“● Erroneous execution …”

† I'll amend my prior comment's “compile-time error” to include “post-compilation error” at link-time as well to support an implementation that stitches together each compilation-unit's borrow-checker directed graphs to build up a whole-program borrow-checker directed graph at link-time, as per “post-compilation error” in the 2nd ¶ under the 1st ● above.

‡ Note the absence of the term “exception” in this sentence which would have been a really good time to utilize it if your definition of exception held.  Note the presence of the term “error” in this sentence instead.