[siknad]

I enjoy writing code with Agda. I like writing APIs that can't be used incorrectly and dependent types are so much more powerful that anything I knew before. Also unicode/custom mixfix operators (if_then_else_) are fun to use. Other languages I've seen just can't offer these things. Probably it is not the best choice to create something you want to run as its ecosystem is not quite developed though, but I also like to reinvent the wheel..

[mbrodersen]

I enjoy programming in Agda as well. However I can’t decide whether to focus on Agda, Idris, LEAN, Coq, F* or Isabell/HOL. There is a lot of overlap but none of those choices seems to have it all.