[Agda] Using Agda in proving computer system correct

[Marko Dimjašević]

Dear Agda community,

I'm still relatively new to Agda and what puzzles me is a sentiment
(that I got by talking to other computer scientists) that Agda is not
well suited for proving complex computer systems correct. Supposedly,
one is to use Coq for such a task instead; people say things like,
"doing non-trivial proofs in Agda is cumbersome".

If that is the case, can you tell why? If one is to do non-trivial
proofs in a constructive manner, what obstacles there are to doing it
in Agda? Are there rough implementation details that are still to be
ironed out? Is there a specific theoretic approach that Agda relies on
that is unsuitable/impractical for writing non-trivial proofs of
computer systems? Is there tool support that is lacking? Is it due to
sub-optimal automated proof search? Is there research still to be done
to make Agda apt for proving properties of computer systems? What is
different with Coq that makes it a good fit?

I'm very keen to both apply and do research in Agda and accompanying
theory for writing constructive proofs of computer systems.
Furthermore, Agda's interface to Haskell (both in terms of the foreign
function interface and the language compiling to Haskell) seems very
appealing and I'm yet to explore this territory; nevertheless, the
interface looks like a (one-way) bridge to Haskell software developers
that are typically not trained in theorem proving.

Your comments would be highly appreciated.


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190803/d6b4bebe/attachment.sig>