Re: [sv-ac] ballot on 1466

Hi Shalom:

Fine.  Let me rephrase:  I know some users who are well aware of the 
thread proliferation problem.  I also know some users who will be 
very happy to have these shorcuts.

The problem of thread proliferation will not be solved by preventing
the shortcuts.

I believe that these shortcuts will improve the ability of human users
to understand and review the code.  I believe that this benefit
outweighs the detraction from possible additional failure modes,
such as the mistake of writing [*] instead of [*2].  

I also concede that reasonable people can diagree about this matter.

J.H.

> Coming to the conclusion that there is a thread proliferation is not
> trivial. I also disagree that 'users are already aware of this problem'
> is sufficient. The understanding of many users about assertions is very
> basic. A theoretical understanding that this can occur is one thing.
> Applying it in practice is quite another. It is quite common for users
> to write code with thread proliferation problems without realizing it.
> 
> Shalom
> 
> > By observing the tool performance and output.
> >=20
> > User's are already aware of this sort of problem,
> > since it is a common mistake to create thread
> > proliferation due to redundancy, e.g. by writing
> >=20
> >    assert property (a[*1:$] |-> b);
> >=20
> > instead of
> >=20
> >    assert property (a |-> b);
> >=20
> > >
> > > How would you expect that a user will notice the thread
> > proliferation?
> > >
> > > > Regarding the argument about dropping a digit and
> > > > accidentally writing [*] instead of [*2], I think
> > > > that, from a user's perspective, it is much more
> > > > likely that this will be caught quickly due to
> > > > the thread proliferation
> > > =3D20
> > > Thanks,
> > > Shalom

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.