From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a0c:a8c5:: with SMTP id h5mr2612069qvc.180.1569334114714; Tue, 24 Sep 2019 07:08:34 -0700 (PDT) X-Received: by 2002:aca:d07:: with SMTP id 7mr153596oin.155.1569334114374; Tue, 24 Sep 2019 07:08:34 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!o24no4710905qtl.0!news-out.google.com!x7ni1608qtf.0!nntp.google.com!o24no4710898qtl.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 24 Sep 2019 07:08:34 -0700 (PDT) In-Reply-To: <5edf39fb-169a-463a-b28e-ece1d3b553e0@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.223.245; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.223.245 References: <5edf39fb-169a-463a-b28e-ece1d3b553e0@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <4fd48d44-ccd5-493c-ae6d-13832b7d7a74@googlegroups.com> Subject: Re: Implementing Rust's borrow checked pointers From: Optikos Injection-Date: Tue, 24 Sep 2019 14:08:34 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader01.eternal-september.org comp.lang.ada:57182 Date: 2019-09-24T07:08:34-07:00 List-Id: 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: >=20 > > > begin > > > A.all ... ; -- raises exception. > >=20 > > No, to be as useful as Rust's borrow checker, instead of raising except= ion, it needs to be a compile-time > > error. The compiler needs to maintain a whole-program directed graph a= t compile-time, not defer a > > detection-based localized analysis to run-time. >=20 > Yes, the compiler would raise that exception at compile time. This idea t= hat 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 =E2=80=9Cerror=E2=80=9D not =E2=80=9Cexception=E2= =80=9D. I just checked; each usage throughout the entire AARM of the term = =E2=80=9Cexception=E2=80=9D are 1) utilized in the context of run-time =E2=80=A2error=E2=80=A2 or 2) the English-language general dictionary definition of exclusion from the= topic being discussed, such as =E2=80=9CThere are a few exceptions to this= general principle=E2=80=9D in the side note in =C2=A72.8. =E2=80=9C=C2=A71.1.5 Classification of =E2=80=A2Errors=E2=80=A2 =E2=80=9CThe language definition classifies errors into several different c= ategories: =E2=80=9C=E2=97=8F =E2=80=A2Errors=E2=80=A2 that are required to be detecte= d =E2=80=A2=E2=80=A2prior to run time=E2=80=A2=E2=80=A2 by every Ada implem= entation; =E2=80=9CThese errors correspond to any violation of a rule given in this I= nternational Standard, other than those listed below. In particular, violation of any rule that uses the term= s shall, allowed, permitted, legal, or illegal belongs to this category. Any program that con= tains such an error is not a legal Ada program; =E2=80=A6 =E2=80=9CThe rules are further classified as either =E2=80=A2compile=E2=80= =A2-time rules=E2=80=A0, or =E2=80=A2post-compilation=E2=80=A2 rules=E2=80= =A0, 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 incorpor= ated into a partition of a program. =E2=80=9C=E2=97=8F Errors that are required to be detected at run time by t= he execution of an Ada program; =E2=80=9CThe corresponding error situations are associated with the names o= f the predefined exceptions. Every Ada compiler is required to generate code that raises the correspondi= ng exception if such an error situation arises during program execution. [I= f such an =E2=80=A2error=E2=80=A2 situation is certain to arise in every execution of a construct, then an implementation is =E2=80=A2=E2=80= =A2=E2=80=A2allowed (although not required)=E2=80=A2=E2=80=A2=E2=80=A2 to report this fact at =E2=80=A2compilation=E2=80=A2 time.=E2=80=A1] =E2=80=9C=E2=97=8F Bounded errors; =E2=80=9CThe language rules define certain kinds of errors that need =E2=80= =A2not=E2=80=A2 be detected either =E2=80=A2prior to=E2=80=A2 or during run time, but if not detected, the range of possible effects shall b= e bounded. The errors of this category are called bounded errors. The possible effects of a given bo= unded error are specified for each such error, but in any case one possible effect of a bou= nded error is the raising of the exception Program_Error. =E2=80=9C=E2=97=8F Erroneous execution =E2=80=A6=E2=80=9D =E2=80=A0 I'll amend my prior comment's =E2=80=9Ccompile-time error=E2=80= =9D to include =E2=80=9Cpost-compilation error=E2=80=9D at link-time as wel= l to support an implementation that stitches together each compilation-unit= 's borrow-checker directed graphs to build up a whole-program borrow-checke= r directed graph at link-time, as per =E2=80=9Cpost-compilation error=E2=80= =9D in the 2nd =C2=B6 under the 1st =E2=97=8F above. =E2=80=A1 Note the absence of the term =E2=80=9Cexception=E2=80=9D in this = sentence which would have been a really good time to utilize it if your def= inition of exception held. Note the presence of the term =E2=80=9Cerror=E2= =80=9D in this sentence instead.