[Agda] Using Agda in proving computer system correct

[Guillaume Allais]

Re your 4th point: you may find a view useful in this scenario.
Here is a proof of concept where such a view is used to define a
proof of decidable equality of size linear in the number of
constructors rather than quadratic.

https://github.com/gallais/potpourri/blob/37e312d9b2b9c95158759754ef1b4a9fdd5f5565/agda/poc/LinearDec.agda

I have also played a bit with software foundations' IMP language,
trying to keep the programs & proofs as short as possible given
that (AFAIK) this is the part of SF where Coq's automation is
supposedly leading to much shorter proofs. In my limited experience,
this seems to be true but views do help us keep things tractable:

https://github.com/gallais/potpourri/blob/master/agda/sf/Imp.agda

Best,
--
gallais

On 05/08/2019 16:17, Jacques Carette wrote:
> 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.
> 
> 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've been reading some Coq proofs (blech) for some stuff in category theory; the
> correspond Agda proofs tend to be shorter and way (way!) more limpid.
> 
> Jacques
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190806/3d41db9b/attachment.sig>