Have you done any Agda, recently?

prodigal_erik · on June 30, 2012

I for one will freely admit that my Haskell still sucks and so I presume I'm not even smart enough yet to start on Agda. Do you recommend it? Do you find it to be (one of) the highest known point on the power continuum?

eru · on July 1, 2012

Oh, I'm still stuck at Haskell, which doesn't suck but could be better. A friend of mine did some playing around with automated proof assistants, and I've been to some talks about seL4, a microkernel prototyped in Haskell, written in C, and proven correct in Isabelle.

From Haskell you can of course go the route to Agda or Isabelle. But Curry is also worth a visit, it combines logical and functional languages.

I, for one, am still learning how to do left-fold based IO in Haskell with enumerators, at the moment.