In my spare time, I like to develop formal mathematics using the proof assistant and programming language Agda. Here is a screenshot of what my latest code looks like:
This is an html-rendering of the latest version of my code hosted here:
https://felix-cherubini.de/sag/Cubical.AlgebraicGeometry.Spec.html
My post is not about the mathematical content – that can safely be ignored for the matter of this post. What I want to show you is, what the code (and the html generated from it) looks like. If you want to look at the source for this file on github, you have to use ‘raw’-view, since github uses the ending to decide, that it should be rendered like a markdown file:
One thing I am constantly dissatisfied with when writing mathematics as formal code, is, that the result is usually far less readable than mathematical articles or textbooks. Most things I wrote recently in Agda, just look like functional source code and should not be too inviting for everyone in my target audience. Of course, when thinking about my math code, I always ask myself, if something working there, carries over to practical programming. I guess in this case I am just rediscovering the fun of something quite old and well known in practical programming.
Until about a month ago, the best remedies for my not so well readable math code, was to extensively use Agda’s mixfix syntax, math symbols via unicode and large comments, sometimes even with diagrams in ascii-art. While my mixfix use turned out to be a bit too much, the other two things work quite ok. However, above I showed you the results of somethin I tried quite late: literate programming!
I learnt how to use Agda’s limited literate programming capabilites together with some pandoc-postprocessing here:
https://jesper.sikanda.be/posts/literate-agda.html
I knew about the literate programming features, but I underestimated the difference it makes. What I use so far, amounts to not much more than having comments, that are rendered to html in some way. The real difference is, that I start with the text explaining what the code is about.
I am pretty sure though, that I would probably not have started to use it so enthusiasticly, if I hadn’t been writing math. This is because literate math coding let’s you mix prose and math code in very much the same way as it is usually done when writing math the traditional way. So one could say that I learnt already how to write literate code in my mathematical education, which allows me now to do it now without too much thinking and discipline.
I do not think, that it is a good idea to write all code like that. In the example above, my goal is to write some interesting math story which leaves out a lot of details which are hidden away. In a practical project, it might help to write, say, the main method in this style to give a top level explanation on how things are organized.
Let me have a pass around my main point again: It helps a lot to have a text file, which also contains code instead of a code file, which also contains text (i.e. comments). It made me think that I am editing a text file, when editing the literate code. Which is great, because it helps against my main problem with comments: I forget to change them, because they are not a part of the code.
Schneide Blog 