[Agda] Using Agda in proving computer system correct

[Nils Anders Danielsson]

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."

However, call-by-name has not been removed entirely.

-- 
/NAD