[Agda] Using Agda in proving computer system correct

[Jon Sterling]

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
>