Add style guide for the PDF

CONTRIBUTING.md

@@ -4,6 +4,8 @@
 
 We are currently aspiring to follow the [Agda standard library style guide][] as much as reasonable. Since some of our code will be rendered into a PDF, the formatting of the PDF takes priority over formatting of the code, so deviations are to be expected.
 
+We also have a separate style guide for formatting the PDF: [PDF style guide](PDF-style-guide.md).
+
 ## Setup with emacs
 
 We use Agda version 2.6.3 and a patched version of the Agda Standard Library; this makes setup more difficult. You can install the correct version of Agda and the stdlib using `nix-env -iA agda -f .`, but this is a global install which you may not want if you also have other Agda projects.

PDF-style-guide.md

@@ -0,0 +1,75 @@
+# PDF spec guidelines
+
+The purpose of the PDF specs is to be readable by a wide range of people. They should not assume
+- knowledge of common (functional) programming syntax and idioms or
+- familiarity with another Cardano-specific resource, other than other specifications.
+
+## Haskell/Agda-isms
+
+We want to avoid syntax that is not commonly used outside of the
+languages we use. While this is really inconvenient sometimes, the
+more we use such notations the more we need to introduce them,
+increasing the barrier to entry.
+
+## Hiding pieces of code
+
+Hiding pieces of the underlying Agda code can be a useful tool to
+accomplish these objectives, but it is important that this is not
+overused. Any code whose meaning depends on hidden code must be
+explained by prose. However, it is always preferable if a figure can
+be fully understood without extra explanation.
+
+## Avoiding complexity
+
+- reduce the number of dependencies as much as possible, which can
+  often be done by generalizing
+- move (simple) definitions from being defined right next to their
+  usage to where they would naturally be defined
+
+## Alignment
+
+For better visual presentation, we should align figures properly. This
+might sometimes not be possible while also maintaining other
+constraints. Two cases where we usually want to align things are:
+- multiple lines of the form `a = b`, where those lines are short enough
+- a long expression of the form `x = a1 + ... + an` should be broken
+  into multiple lines where the `=` and `+` signs are aligned (also
+  applies to any other infix operator)
+
+The second point shouldn't be overused - if it is possible to use
+horizontal space and save on vertical space it is probably good to do
+so.
+
+## Cardano-specific terms
+
+We prefer generic naming over Cardano-specific naming. The main
+example is `Coin` (instead of `Lovelace`).
+
+## Prose explaining figures
+
+The prose should supply context and should help understanding the
+figures. Generally, for each definition we should answer the questions
+what and why.
+
+- For what, note that not everything that's contained in a figure
+  necessarily needs an explanation - if the explanation of a
+  definition is simply repeating the definition in words it can
+  probably be omitted (like comments in a program). This ensures the
+  prose is relevant: a reader that reads lots of unnecessary
+  explanations is likely to skip reading the prose at some point. But
+  then why write it in the first place?
+
+- Why is a much more difficult question to answer, and also not every
+  single definition needs a direct answer to this question. Instead of
+  answering 'why do we need X' directly, it might be better to explain
+  something about the greater design that explains why we need 'X, Y
+  and Z' all at once.
+  This question can also have other shapes: why did we define it as X
+  instead of Y, why does this case need special handling, etc.
+
+Other notes:
+- repetition in the prose should be avoided
+- the relations (and often the functions as well) in the spec don't do
+  things, they define things (ex: '`feesOK` defines what conditions
+  the transaction fees must satisfy', not '`feesOK` computes whether
+  the conditions that the fees must satisfy are being met')