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

[Andreas Abel]

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/