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 Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED.fn3LatRFkm9/xzEj7F2/NQ.user.gioia.aioe.org!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Intervention needed? Date: Tue, 2 Apr 2019 10:30:23 +0200 Organization: Aioe.org NNTP Server Message-ID: References: <6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com> <6f9ea847-2903-48c8-9afc-930201f2765a@googlegroups.com> <87a7hgvxnx.fsf@nightsong.com> <4e240c66-dce8-417f-9147-a53973681e29@googlegroups.com> <28b6a472-6c3a-40a6-8a96-2e27a65ab2ef@googlegroups.com> NNTP-Posting-Host: fn3LatRFkm9/xzEj7F2/NQ.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 Content-Language: en-US X-Notice: Filtered by postfilter v. 0.9.2 Xref: reader01.eternal-september.org comp.lang.ada:56045 Date: 2019-04-02T10:30:23+02:00 List-Id: On 2019-04-01 23:42, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:q7tfi3$1483$1@gioia.aioe.org... >> On 2019-04-01 17:13, Optikos wrote: >> >>> One clarifying question that I have is: how would you "prove no >>> Constraint_Error propagating"? At run-time or at compile-time or at >>> engineering-time using tools other than the compiler? >> >> It must be the compiler. The programmer states contracts of the >> subprograms and if the contracts cannot be proven to hold that is a >> compile-time error. >> >> The problem is, of course, specifying the mandatory strength of a proof >> AKA false negatives vs. false positives. If a fact cannot be proven true >> by one compiler that makes the program illegal even if another compiler >> could prove it. > > The problem with that is that in the canonical Ada description, it's always > possible for a check to fail. One would need to describe in precise terms > what "optimizations" of checks that a compiler is mandated to do, or the > "proof" would be pointless. That is, in the hypothetical: > > function Foo return Natural > with Exceptions => null is (0); > > this is illegal in the general case, since this function can raise > Constraint_Error (from the conversion of the literal to Natural) and > Storage_Error (since everything can raise Storage_Error). The conversion will have a contract not to raise if the argument is 0. The Storage_Error contract will be conditional: no Storage_Error when stack has N free storage units free. You could then prove the program is safe with 10KB of stack. > One could imagine trying to invent a set of rules of which check > optimizations have to be made (a conversion of a literal to a subtype only > raises an exception if it actually out of range; a conversion of an object > of a subtype to the same subtype never raises an exceptions; and so on), but > such a set of rules would either be massive and put a lot of burden on > compilers (especially existing compilers), or would be full of holes and > thus little could be written this way. Sure. It will be a lot of work to contract *all* built-ins. This is another reason to reduce them drastically, thus my plea for a type system overhaul. The language core must have contracted. The libraries may have weaker contracts. > My preference for this check is to make it implementation-defined (possibly > with a few minimum requirements). Thus, one compiler might be able to > compile Foo and another would not -- but it would reflect reality. A > compiler that is smarter about checks would be able to handle more code, all > the way up to the level of SPARK (where most code could be proved to not > raise exceptions). That is a compiler vendor POV. As a programmer I want the opposite. I want to be able to have proofs as a part of my program. > For Janus/Ada, I'm working toward having (optional) warnings for the raise > of any exception; that, combined with warnings-as-error mode can give the > effect of preventing any exceptions other than ones explicitly expected. > It's pretty much all that can be done within Ada as it stands. But that is > not as good as an exception contract (especially as exceptions that you want > to raise become a pain). Right, and unanticipated exceptions is a major contributor of bugs in Ada. It is not so that exceptions cause bugs, rather bugs manifest themselves as exceptions. If one could contract them most of the bugs will not pass through the compiler. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de