[Agda] Using Agda in proving computer system correct

[Roman]

“Using Coq is like doing brain surgery over the telephone.” – Peter Hancock

That was my experience with Coq as well. I think Agda's reflection
machinery (and the Idris' one for that matter) is highly
underappreciated, one can do wonders with it as it gives you first
class access to internals of Agda, including the ability to declare
functions, quote data type definitions, infer/check types and deal
with metavariables. The `TC` monad and the `macro` gadget are some
really nice and intuitive things.

However library support is almost non-existing. There are several
libraries that deal with reflection (most notably the Ulf's
`agda-prelude`), but most of them (if not all) are either dead (i.e.
do not even build) or undocumented.

I learned how to use reflection through trial and error and was able
to implement the equivalent of Haskell's `deriving Eq`, only for
decidable equality and with full support of
dependent/higher-order/indexed data types with implicits, instance
arguments, irrelevance and universe polymorphism [1], which showcases
that Agda's reflection is quite powerful. Others have implemented ring
solvers [2] [3] [4], rewrite as a tactic [5], another `deriving Eq`
[6] and various other stuff. Still, library support of general
metaprogramming tools is lacking. I also wasn't satisfied by naked and
raw De Bruijn indices that Agda uses for its internal representation
(which is very error-prone and inefficient) and not having static
information on how many times a term was quoted was quite unpleasant,
but these are technical details that are pretty solvable. Additional
features like defining data types using reflection also can be added.

What is harder to fix is that Agda since its creation hadn't been
scaling well (I stopped paying attention a couple of years ago, so I
don't know whether things have changed or not). 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. People have reported that their projects required
a dozen or two of GBs 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). I
can't count for how many times I was thinking "ok, I'll wait a bit
more and kill the process". It is quite discouraging to develop
something for months just to figure out that you can only test it on
completely trivial things, because otherwise type checking won't
finish. Again, I don't know whether the situation has been improved in
recent years.

So for me performance was a deal breaker, not theoretical limitations.

Does Agda still implement call-by-name reduction strategy (as opposed
to call-by-need)?

[1] https://github.com/effectfully/Generic/
[2] https://oisdk.github.io/agda-ring-solver/README.html
[3] https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Solver/Ring.agda
[4] https://github.com/UlfNorell/agda-prelude/blob/master/test/DeriveEqTest.agda
[5] https://github.com/UlfNorell/agda-prelude/blob/master/test/Reright.agda
[6] https://github.com/UlfNorell/agda-prelude/blob/master/test/DeriveEqTest.agda