Re: Interesting article on ARG work

[Bojan Bozovic <bozovic.bojan@gmail.com>]

On Friday, April 6, 2018 at 12:12:04 AM UTC+2, Randy Brukardt wrote:
> "Bojan Bozovic" <bozovic.bojan@gmail.com> wrote in message 
> news:17b6d5b9-5909-4f0c-ab25-9b3cf4fd0450@googlegroups.com...
> ...
> > Ah I was victim of April the 1st joke! I wasn't joking though. My
> > proposal was to add assertions in general to Ada, as something in
> > the core language, like exceptions are, or tasks, which would
> > function just as "ghost code" you had in mind when
> >
> > pragma assertion_policy (check);
> >
> > is used. Maybe not use assertion keyword but use functions with
> > ghost? I really can't say which approach wold work best, from the
> >  point of function, readability and conciseness. That is for ARG to
> > decide.
> 
> But what would the point be? A pragma is a first-class part of the language 
> (it's not optional!). And a pragma can be used in places that a statement 
> cannot be used (that is, with declarations). To get even equivalent 
> functionality that way would be fairly complex (needing both statements and 
> declarations). Sounds like a lot of work for very little gain.
> 
> Personally, I don't see a lot of value in pragma Assert in the first place 
> (as opposed to the other contract assertions). I'm in the camp that 
> suppressing/ignoring checks ought to be a last resort, only to be used when 
> performance goals can't be met any other way (using a better algorithm is 
> always a better way). As such, "cheap" assertions might as well just be part 
> of the code; I would never want to remove them. Often, the compiler can 
> prove that they're true (so there is no cost), and if not, a well-defined 
> failure is better than erroneous execution where anything can happen.
> 
> For instance, the Janus/Ada compiler has a lot of code like:
>       if Node.Solution = null then
>            Internal_Error ("Missing solution");
> 
> This could have been modeled as an assertion:
> 
>     pragma Assert (Node.Solution /= null, "Missing solution");
> 
> but the above modeling allows calling a fairly complex error management 
> routine (which, if trace mode is on, gives the user various interactive 
> debugging options). And we wouldn't want to remove the check in any case; 
> it's much better to detect the problem in a controlled way rather than an 
> uncontrolled one (especially if all checking has been suppressed).
> 
> Some assertions are expensive to run, and thus shouldn't run all of the 
> time. For those, I generally find that it is best to tie them to the 
> debugging mode for whatever subsystem that they are related to. (Pretty much 
> every program I write has a variety of debugging modes, so that one has a 
> limited amount of debugging information to look through to find problems. I 
> usually write my programs with a substantial amount of debugging from the 
> start, and then usually keep any debugging added to find specific problems. 
> Whenever I haven't had substantial debugging, I've always found I've had to 
> add it, in order to get any confidence that the code is doing the right 
> thing.) Since there are multiple such debugging modes, tying everything to a 
> single "check/ignore" flag is much too coarse for my purposes. So again 
> there isn't much use for pragma Assert.
> 
>                          Randy.

If assertions/invariants encompassed type invariants and were used in loops as well, like in Eiffel, readability would be better in my humble opinion, while Ada have pragma assert that can be used in loops, and static_predicate and dynamic_predicate on types.

Maybe assertion blocks would work better as in Eiffel for loops? Like exception block in Ada?

Eiffel approach must have been discussed by ARG, however readability is still important for human programmer, even though it isn't important for the compiler.