[Agda] Using Agda in proving computer system correct

[mechvel at scico.botik.ru]

On 2019-08-05 16:28, 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.


There is the DoCon-A library for algebra (see it on the Web) which 
cannot be type-checked by Agda in less
than 13 Gb memory.
I have reported of this earlier.
Probably this library is larger than other libraries in Agda, but it is 
much smaller than many other libraries for computer algebra. I am not 
sure, I suspect that this unnatural type check cost is due to some 
deficiency in the type checker design/implementation. Because everything 
looks natural in the library code itself.


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

Indeed, this is a library issue.
* Regularly, Natural needs to be represented in Agda as a list of 
macro-digits, and still some small number of operations on a macro-digit 
will need to be built-in.
* Also in lib-1.1 printing a natural number in decimal digits is fast, 
this is due to a built-in division with remainder.

--
SM