I think agda has really nice syntax. And indeed, the language itself is quite nice. However, the standard library is littered with tons of unicode symbols. These are effectively un-typable in most editors. The dev’s position is that you should use their emacs plugin which converts ascii digraphs and trigraphs into symbols (as if they were ligatures). However, those of us who don’t use emacs (all 95% of us) are SOL. Given that most of these symbols are typed as digraphs anyway, this whole thing is just an exercise in aesthetics.
Totally unrelated but I’m irresistibly reminded of the classic Swedish song “Hönan Agda” by Cornelis Vreeswijk where a cock relentlessly pursues (literally hen-pecks) the titular hen Agda in order to get her naked for sexual congress.
Sorry, not totally unrelated. It’s just one member of a whole family of dumb Coq jokes.
Haha, I honestly did not know that!
Anyone has idea how does F* compare?
I like the flexibility of Coq’s approach. You just export to your language of choice and then you are free to deal with unprovable or non-total parts of the program like I/O as you want.
That said, I haven’t used any of them for a real life program yet.