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

[Andrea Vezzosi]

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