One thing I love about Agda is that it translates to Idris (which is much more friendly to a regular programmer) almost mechanically.<p>Once I needed to write a proof of permutation transitivity in Idris. I’m not smart enough to write it myself, but I found a proof in Agda and translated it to Idris in 20 minutes. <a href="https://github.com/stepancheg/idris-sort/blob/master/PermHard.idr" rel="nofollow">https://github.com/stepancheg/idris-sort/blob/master/PermHar...</a>
Reminder that <i>all</i> ACM Digital Library resources, including books, are free until June 30.<p><a href="https://www.acm.org/articles/bulletins/2020/march/dl-access-during-covid-19" rel="nofollow">https://www.acm.org/articles/bulletins/2020/march/dl-access-...</a>
I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light.<p>Ref: <a href="https://cs.stackexchange.com/questions/122066/does-the-underlying-computational-calculus-in-type-theories-affect-decidability" rel="nofollow">https://cs.stackexchange.com/questions/122066/does-the-under...</a>
thx a lot, found some other interesting books along the way!<p><a href="https://dl.acm.org/acmbooks" rel="nofollow">https://dl.acm.org/acmbooks</a>