[Agda] Using Agda in proving computer system correct

[Guillaume Allais]

Hi Jon,

The implementation has a lot of comments:
https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Reduce/Fast.hs

Cheers,
--
gallais

On 05/08/2019 15:27, Jon Sterling wrote:
> 
> 
> On Mon, Aug 5, 2019, at 9:28 AM, Nils Anders Danielsson wrote:
>> On 03/08/2019 23.11, Roman wrote:
>>> It was the case that you could type check things in almost no time,
>>> then open some module (without using anything from it) and wait for
>>> two minutes for type checking to finish.
>>
>> If you have some example where Agda exhibits terrible performance,
>> please report it on the bug tracker.
>>
>>> People have reported that their projects required a dozen or two of
>>> GBs of RAM.
>>
>> I have written on the order of 100 000 lines of Agda code, and I think I
>> can typecheck all of it (excluding pieces that have bit-rotted) using
>> less than 3 GB of RAM.
>>
>>> Even something as simple as printing a natural number had terrible
>>> performance (I think it even was exponential?) for many years (which
>>> has been fixed rather recently).
>>
>> This was a library issue, rather than a more fundamental problem, right?
>> (Not that libraries aren't important.)
>>
>>> Again, I don't know whether the situation has been improved in recent
>>> years.
>>
>> There have been lots of improvements over the years, but things can be
>> improved further.
>>
>>> Does Agda still implement call-by-name reduction strategy (as opposed
>>> to call-by-need)?
>>
>> Here's the abstract of a talk Ulf Norell gave at AIM XXVII:
>>
>>    "Since the olden days, Agda has been using a substitution-based
>>    call-by-name evaluation strategy with all the associated problems. In
>>    this talk I will describe my efforts to bring Agda into the late
>>    1980's: introducing the Agda Abstract Machine. The abstract machine is
>>    an environment-based call-by-need machine, solving both the
>>    substitution problem and the call-by-name issue. Some interesting
>>    challenges are introduced by the fact that we evaluate open terms, and
>>    are constrained by the existing term representation of Agda."
>>
> 
> This sounds like a fascinating talk; are there any notes or slides available?
> 
> Thank you,
> Jon
> 
> 
>> However, call-by-name has not been removed entirely.
>>
>> -- 
>> /NAD
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>