Nice list! For proofs I've been finding the leap into dependent-type theory to be very productive as many provers in this realm also double as practical progra

Nice list! For proofs I've been finding the leap into dependent-type theory to be very productive as many provers in this realm also double as practical programming languages allowing the possibility of shipping proof-carrying code. My two favorites in this area are Lean [0] and Agda [1], the latter of which recently received a nice introductory text from Phil Wadler and Wen Kokke [2]. [0] https://leanprover.github.io/ https://leanprover.github.io/ [1] https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php [2] https://plfa.github.io/ https://plfa.github.io/