[Agda] Using Agda in proving computer system correct

[Matthieu Sozeau]

Hi everyone,

  Interesting discussion! I don’t think you need to be a brain surgeon to
program in Coq (I wouldn’t trust an arbitrary Coq user with my brain in any
case :), but it’s true it can easily be misused (the video-game effect of
the tactic mode in particular can be pretty bad). In my opinion however
what is true for Coq is also true for Agda, type theory cannot scale up to
large verification problems without good abstractions: whether they are
robust tactic languages avoiding the nitty-gritty of proof terms
(maintaining an Agda development written without abstractions by someone
else is not more fun or easy than a fragile Coq proof script), or using the
highly-expressive type systems we have to express ideas concisely and
efficiently. I think these two can work hand-in-hand actually: an example
being the treatment of views and the reflect predicate of ssreflect in Coq
for example, which leverages dependent elimination and computation and
integrates it with a tactic language construct to seamlessly move between
different specifications about a given function. Likewise, the rewrite
construct of Agda, provides a higher-level ‘tactic’ during programming,
inferring a rewriting predicate and applying it using the eliminator of
equality, just like the rewrite tactic of Coq does.

  Abstractions can be costly to compilers but I would guess the main
differences in performance between Agda on one side and Coq and Lean on the
other side would rather be in the conversion / reduction algorithms and in
unification, where they are mostly incomparable right now, although getting
closer in some respects (e.g. the use of abstract to block reductions).

Le lun. 5 août 2019 à 11:17, Jacques Carette <carette at mcmaster.ca> a écrit :

> I can't help but comment on a mis-perception in this particular message
> earlier in this thread:
>
> On 2019-08-03 4:47 p.m., Xuanrui Qi wrote:
> > Also, it's widely agreed that tactic-based proofs and backwards
> > reasoning are definitely more suited for large-scale proof efforts. As
> > a result, most if not all large mechanized computer system
> > verifications proof efforts use proof assistants with LCF-style tactic
> > language (CompCert and CertiKOS in Coq, seL4 in Isabelle, CakeML in
> > HOL4, etc.)
>
> It used to be "widely agreed" that dependent types were too hard for
> doing anything of any size - this has been thoroughly debunked. Same
> with the meta-theory of binders. Lots of hard work had to be done to
> figure out 'how to do it', but out of that hard work techniques were
> distilled so that it no longer is so hard.
>
> Tactics originate from the LCF view of proofs as abstract objects that
> you cannot reach in to; they are 'proof transformers'. And they are
> absolutely necessary if your proofs are in Prop. And having proofs in
> Prop itself originates from classical mathematical ideas that "proofs
> have no content" and the "widely agreed" (!) idea that carrying
> irrelevant proofs around will produce a system that is much too slow.


For what it’s worth, despite having proofs in Prop in Coq (or Lean), they
are still around in memory (albeit blocked by Qeds usually, and sometimes
lazily loaded from disk). So the view of Prop as a bracket of Type,
reconciling with the Agda/HoTT-style view of proofs as by default relevant
(and maybe just squashed/truncated explicitely when irrelevance/erasure
matters or impredicativity is used) would not change much w.r.t. the space
efficiency story — a definionally proof-irrelevant sort (OTT’s Prop, SProp)
does change the time-efficiency story significantly however, as terms
standing for proof terms (in SProp) must never be converted in this case.
Also, Agda uses call-by-name or call-by-need reduction (Coq uses a variant
of call-by-need in its default conversion algorithm), so unfolding of
proofs usually happens only if necessary and they shouldn’t differ much
(the devil’s in the details of course).

But, well, Agda's notion of proof, as embedded as specific terms in Set,
> is not proof-irrelevant. And, lo and behold, dependent pattern-matching
> makes that extremely useful! All of a sudden, what used to be
> complicated tactics are now just normal programs. This is a major
> advance. (See http://r6.ca/blog/20171008T222703Z.html for reflections of
> a Coq expert 'discovering' this.)
>
> Having said that, there does remain issues worthy of further research IMHO:
> 1. ssreflect-style reflection, or the "local approach" to reflection.
> There really are times when a domain has decision procedures based on
> the *syntax* of its terms based on some (usually quotiented)
> term-algebra; think polynomials over Nat and their normal form as a
> decision procedure for semirings [i.e. pure arithmetic induces proofs
> via an interpretation]. Calling these 'tactics' obscures much of the
> reason for the power of the method.
> 2. global style reflection (see the work of William M. Farmer). For when
> you want to embed all of your language. This is what MetaCoq is trying too.
> 3. "sufficient lazyness" -- i.e. figuring out when both values (which
> can be proofs) and control paths are no longer needed, and just erasing
> them. [See https://arxiv.org/abs/1907.13227 but also
> http://sci-hub.tw/10.1145/115866.115890 which links back to ideas of #2
> for really interesting ideas from generic PL in that direction]
> 4. more automation. Yes, it is painful to do a case-split into > 100
> cases [yes, I have such code], where only 4 require a non-trivial
> sub-proof [and even then], and the rest of the ~100 cases are just
> 'refl'. Or maybe the answer isn't automation, it's some eta-like rule
> for inductive types -- who knows.


I think the view pattern can help here, using dependent elimination to let
the typechecker know only a handful of cases are interesting and the rest
are treated the same, e.g. using predicates of the form:

data MyCases : MyType -> Set where
  interesting a b : MyCases (foo a b)
  interesting2 : MyCases bar
  notsointeresting m : ~ (is_foo_or_bar m) -> MyCases m.

Then:

mycases m : MyCases m
mycases (foo a b) = ...
mycases bar = ...
mycases other = notsointeresting m refl

You’ll do a full case split one time only this way.
Again it’s a matter of using the right tool for the job, and type theory
provides plenty of options!
I guess Coq gives more options to brute force such proofs using the tactic
language, but in the long term such methods don’t scale well.

Best,
— Matthieu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190806/86a89069/attachment.html>