[Agda-dev] One more point for my false-golfing score

[Ulf Norell]

I would be all for removing 'abstract'.

/ Ulf

On Wed, Jul 1, 2015 at 9:40 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> What positivity do postulates get?
>
> On Wed, Jul 1, 2015 at 9:07 PM, Andreas Abel <abela at chalmers.se> wrote:
> > On 01.07.2015 17:49, Wolfram Kahl wrote:
> >>
> >> On Wed, Jul 01, 2015 at 08:21:58AM +0200, Andreas Abel wrote:
> >>>
> >>> Subject: [Agda-dev] One more point for my false-golfing score
> >>>
> >>> -- https://code.google.com/p/agda/issues/detail?id=1599
> >>>
> >>> data ⊥ : Set where
> >>>
> >>> abstract
> >>>
> >>
> >> Nice to know that ``abstract'' is not only a premature optimisation,
> >> but also unsound.
> >>
> >> (I used ``abstract'' my early Agda2 days to get more theories
> >>   trough my memory constraints, but as Agda got better,
> >>   at some point its advantages essentially disappeared,
> >>   and its disadvantages made me abandon it,
> >>   so I am not using ``abstract'' anymore.
> >> )
> >
> >
> > Thanks for the feedback.  "abstract" lacks a theory, so I am not too
> > surprised it is unsound.  It also has seen limited use, probably also
> since
> > it does not work reliably.
> >
> > The API for abstract things is very confusing, I just spend hours trying
> to
> > understand what is going on inside of Agda.  Basically, if you ask for
> > information about an abstract identifier and you are not in abstract
> mode,
> > you get the answer that it is a postulate.  That lead to the failure of
> > positivity checking---there is nothing to check about postulates after
> all.
> > The problem was that the abstract mode had not been entered when it came
> to
> > check these abstract definitions.
> >
> > Here it shows that Agda does not have a safe kernel.  If safety checks
> like
> > positivity are omitted by accident of the programmer, Agda happily still
> > lets you use the (uncertified) definition and prove False in sequence.
> >
> > In the long run, such a design is not sustainable.  There will be no end
> to
> > exploits.  Without proper double-checking facilities or internal
> > certificates Agda will never be safe.
> >
> >> If you take out the ``abstract'' and the indentation,
> >> you get a positivity-check error message that sounds like
> >> it might be ``fixed'' even for continued use of ``abstract''...  ;-(
> >
> >
> > I did not understand what you meant by this.
> >
> > Cheers,
> > Andreas
> >
> > --
> > Andreas Abel  <><      Du bist der geliebte Mensch.
> >
> > Department of Computer Science and Engineering
> > Chalmers and Gothenburg University, Sweden
> >
> > andreas.abel at gu.se
> > http://www2.tcs.ifi.lmu.de/~abel/
> > _______________________________________________
> > Agda-dev mailing list
> > Agda-dev at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda-dev
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150701/6222fd10/attachment.html