[Agda] Using Agda in proving computer system correct

[Xuanrui Qi]

Metaprogramming is a powerful tool and Agda/Idris style metaprogramming
is enough to implement a powerful tactic system like Coq's. For this
matter, Idris has the library Pruviloj (
https://github.com/idris-lang/Idris-dev/tree/master/libs/pruviloj) that
works basically like Mtac, although Pruviloj is still pretty limited at
the current point (mainly due to the lack of active development
effort). 

Agda's reflection mechanism is certainly strong enough for one to do
the same, but I agree that the main problem here is the lack of library
support. For example, AFAIK there's no mechanism in Agda that works
like like elaborator reflection in Idris. Sure we can do the same
things using Agda's reflection mechanism, but with a lot of extra
effort.

Of course, we all hope that one day we would have a programming
language/proof assistant that works equally well as a dependently-typed 
programming language and as a (tactic-based) interactive theorem
prover. We already have a lot of work towards this (e.g. Program and
Equations in Coq to improve DTP, elborator reflection in Idris &
reflection in Agda to support tactics-style reasoning). But what we
really need now, IMO, is better tool support for all of this.

-Xuanrui

On Sun, 2019-08-04 at 00:11 +0300, Roman wrote:
> “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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda