[Agda] Using Agda in proving computer system correct

[Jacques Carette]

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