[Agda] Using Agda in proving computer system correct

[Jason -Zhong Sheng- Hu]

my coin here is to point out that it is not necessary that Coq beats Agda by far in development speed. It turns out that Coq and Agda are good at problems in their specific domains.

for example, due to dependent pattern matching, Agda does better job at proofs requiring large chunks of inversions; in those cases, there won't even be cases generated.

another domain in which Agda beats Coq is when complex inductive scheme is necessary. termination checker in Agda is significantly more permissive than Coq's. Agda permits mutual simultaneous induction while in Coq, proving such kind of inductive schemes requires significant effort.

Equations shows very good potential to fill up but at this moment, Equations is still too buggy to take the role. not to mention that its lack of Emacs interaction.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Xuanrui Qi <xqi01 at cs.tufts.edu>
Sent: August 3, 2019 8:03 PM
To: Roman <effectfully at gmail.com>; Nils Anders Danielsson <nad at cse.gu.se>
Cc: agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: Re: [Agda] Using Agda in proving computer system correct

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

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190804/27741b01/attachment.html>