[Agda] Using Agda in proving computer system correct

[Xuanrui Qi]

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.)

Agda can potentially be as competitive once we get a good tactic
language.

However, if you want to verify a purely-functional piece of systems
software, maybe Agda is the way to go. You can use dependent types to
encode the desired properties and construct a correct-by-construction
version of your program (though performance might become an issue).
Usually this is difficult though.

-Xuanrui

On Sat, 2019-08-03 at 21:22 +0200, Nils Anders Danielsson wrote:
> On 03/08/2019 10.05, Marko Dimjašević wrote:
> > Is it due to sub-optimal automated proof search?
> 
> I don't know what the people you talked to had in mind, but this
> could
> be one thing. Libraries might be another.
>