Agda Writer

My student Marko Koležnik is about to finish his Master’s degree in Mathematics at the University of Ljubljana. He implemented Agda Writer, a graphical user interface  for the Agda proof assistant on the OS X platform. As he puts it, the main advantage of Agda Writer is no Emacs, but the list of cool features is a bit longer:

  • bundled Agda: it comes with preinstalled Agda so there is zero installation effort (of course, you can use your own Agda as well).
  • UTF-8 keyboard shortcuts: it is super-easy to enter UTF-8 characters by typing their LaTeX names, just like in Emacs. It trumps Emacs by converting ASCII arrows to their UTF8 equivalents on the fly. In the preferences you can customize the long list of shortcuts to your liking.
  • the usual features expected on OS X are all there: auto-completion, clickable error messages and goals, etc.

Agda Writer is open source. Everybody is welcome to help out and participate on the Agda Writer repository.

Who is Agda Writer for? Obviously for students, mathematicians, and other potential users who were not born with Emacs hard-wired into their brains. It is great for teaching Agda as you do not have to spend two weeks explaining Emacs. The only drawback is that it is limited to OS X. Someone should write equivalent Windows and Linux applications. Then perhaps proof assistants will have a chance of being more widely adopted.

5 thoughts on “Agda Writer

  1. 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.

  2. 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.

  3. 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).

    1. 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.

Leave a Reply to Mike Shulman Cancel reply

Your email address will not be published. Required fields are marked *

*