Re: Press Release - Ada 2012 Language Standard Approved by ISO

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 21 Dec 2012 19:40:57 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:14oqoq06zhlu2.tcasif3hdyhw.dlg@40tude.net...
> ...
>> In essence 1 and 2 are about knowing something statically, during
>> compilation. Not necessarily the constraint itself, which may be dynamic,
>> yet allowing to prove something statically, e.g. that array index is 
>> always within the bounds.
> 
> Well, I obviously disagree about that. Constraints, in my view are all about 
> *introducing* checks. Predicates just provide an extension of that.

We mean different "checks" here. As you have explained below, you mean a
"true" check, a thing that never fails. I meant a dynamic check, a thing
that is not statically true and need to be approached in the implementation
according to the outcome. That evil thing is to be eliminated by
introducing good things, "true checks."

>> I don't see how predicates might be helpful for either 1 or 2.
> 
> I don't see how range constraints would be helpful for either 1 or 2.

   procedure Foo (S : String) is
      subtype I is Integer range S'Range;

>>   subtype Even is Positive with Dynamic_Predicate => Even mod 2 = 0;
>>   subtype Each_Second_Character is String (Even);
>>
>> won't work. What I see is a yet another way to pack implementations into
>> declarations as Georg promptly suggested, a slippery slope...
> 
> You believe checks are part of the implementation, while I believe that they 
> are something separate. There is is no real hope of agreement on that, so I 
> fear there isn't much point in discussing it. But I'll try for a moment...
> 
> Checks, in my view, are things that should never fail in a correct program. 
> Thus, they should not be considered part of the implementation; they're 
> something separate. Indeed, the only reason that they are made dynamically 
> is because checking them statically is beyond the current state of the art. 
> (I would hope that by the time the next version of Ada rolls around, that 
> will no longer be true.)
> 
> Your argument about them being part of the implementation comes from the 
> fact that Ada confuses the role of exceptions and handlers that come from 
> checks vs. those that are part of the semantics (like End_Error). IMHO, it's 
> wrong to be handling exceptions raised by checks; these represent bugs and 
> must be eliminated from the program, not handled. (Handling them just covers 
> up bugs.) For Ada 2012, you can differentiate exceptions somewhat by what is 
> present in constract aspects (preconditions, predicates, etc.) - which 
> always represent checks, but of course that's not quite complete. And there 
> is a similar problem for handlers: there are "last chance" handlers (which 
> capture all exceptions outbound), these aren't clearly separated from those 
> handlers which are semantic in nature. Last chance handlers are necessary 
> for all exits, of course, but they have nothing to do with the failed check 
> (the check remains failed at the end of such a handler) . (GNAT does this 
> better with their "at end" handler, but of course that's not Ada.) These are 
> language flaws, not fundamental to the model.

Ah, but we are in a full agreement here.

What I said was: IF a "check" is dynamic THEN that must be an
implementation. Since a true check may not fail. Then a fluttering "check"
is something else. Bug, or an intended behavior, it is a part of the
implementation.

> In an ideal world, all of these "checks" will get made statically. Hopefully 
> that's coming. In mean time, it's important to get programmers used to the 
> idea of writing checks this way, so that future tools can make the checks 
> statically (there is no hope of making checks statically if they are just 
> written in natural language comments).

OK, this is rather a tactical disagreement then. Ada's stance was
conservative, not eager adding features impossible to implement properly.
Because somebody (Georg) could readily base his design on the faulty.

In the first step I would rather prefer means to declare user-defined
operations pure, context-dependent pure, compile-time evaluated etc. This
would be more universal than mere predicates, and "proper" predicates would
require that stuff anyway. An alternative, letting the compiler/vendor to
deduce such properties, is IMO unrealistic (an undecidable problem, I
think).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de