Is Emacs really that bad? Obviously it has a lot of features that the average user isn't going to make use of, but my impression was that recent versions of Emacs should be usable just like an ordinary word processor / text editor, now that the Emacs developers have fallen in line with the rest of the world on issues like the meaning of "End" and so on. What is it about Emacs that takes 2 weeks to explain?

If someone came to me with a plan for something like this, my first inclination would be to suggest putting the effort into improving the Emacs Agda-mode instead. Most of the extra features you mention should be implementable inside Emacs with a little work.

Emacs is in fact a highly exotic piece of software simply because it is a text editor. More importantly, consider the fact that Python, Java, C/C++, LaTeX, Ruby, etc. are never ever tied to a single text editor, whereas Agda is tied to Emacs. That is a huge hinderance to adoption of Agda. It has nothing to do with how good or bad Emacs is. Having to use a specific editor just to write code for Agda is a ridiculous requirement.

There is a second editor - atom, now. Even better, the write of that (Ting-Yan Lai) has actually documented the interaction between agda and an editor at

https://github.com/banacorn/agda-mode/wiki/Conversations-between-Agda-&-agda-mode

I have never managed to find this in the Agda wiki (or any details of the .agdai format)

It is worth mentioning that Coq has had CoqIde for a long time, so if (like me) you are a Vim user and vehemently opposed to using Emacs, then it is a great option to have.

I have defined these simple bindings defined in CoqIde's GTK config file, which provides the vast majority of the UTF8 you'd actually want to use for basic logic, numeric inequalities and writing out types. (N.B. the logical negation character ¬ comes on UK keyboard as standard.)

bind "F9" {"insert-at-cursor" ("→")} bind "F11" {"insert-at-cursor" ("∀")} bind "F12" {"insert-at-cursor" ("∃")} bind "<shift>F9" {"insert-at-cursor" ("λ")} bind "<shift>F11" {"insert-at-cursor" ("∨")} bind "<shift>F12" {"insert-at-cursor" ("∧")} bind "<ctrl>F9" {"insert-at-cursor" ("≠")} bind "<ctrl>F11" {"insert-at-cursor" ("≤")} bind "<ctrl>F12" {"insert-at-cursor" ("≥")} bind "<ctrl><shift>F9" {"insert-at-cursor" ("↔")}

(In case you can't read that, the listed symbols are: implication [right arrow], universal quantifier [for all / upside down A], existential quantifier [there exists, backwards E], lambda [greek letter], vel [logical OR / like a V], wedge [logical AND / upside down V], not equals [equals with stroke through], less than or equal, more than or equal, bi-implication [two-way arrow].)

These are much better shortcuts than writing out LaTeX names, and allow you to type out proofs a lot more naturally and faster. If you want a more exotic/uncommon symbol you can just copy and paste it in, which is actually very easy in a normal editor. Or you could go and create your own keyboard layout to switch in and out of for greeks and so on, or use an on-screen character map tool. With a custom IDE you might prefer a toolbar you can just click on for various symbols.

Regardless, it is quite clear that the lack of editors has nothing to do with the popularity of proof assistants. It has a lot more to do with writing proof checked programs being incredibly difficult, tedious and slow work, compared to just writing code contracts and unit testing etc. However, with awful 'Agile' code development methodologies already being widespread, there isn't even any time for test-driven development or up-front design work any more, never mind producing certificates of correctness. You must simply 'write the code', every day, for your weekly 'sprint'. It is very depressing. Maybe if you're a superstar/oracle of knowledge, you can do all your proofs in half a day, and convince your manager it's worthwhile, despite it making all your code unmaintainable for any less skilled person, since the proofs will stop working and they won't be able to fix it, and by implication, there won't be any normal unit tests to check it still behaves properly otherwise. For anyone else it's hopeless.

Anyway, I too would like to see this editor ported or just rewritten as cross-platform for Windows & Linux, because as it is, on OSX only, it may as well not exist for most people, including a lot of those that might wish to improve/maintain it, who aren't likely to want overpriced Apple products (except for cross platform testing, or to work on iOS stuff).

I think there's an Atom plugin for Agda that works on Windows and Linux. I am afraid there is close to zero chance that the original author of Agda Writer (or me) would port it to Windows and Linux. It uses all the OSX technology, and is implemented in Objective C.