Discussion: Levels of detail in human-readable document

This discussion issue continues a thread started in #752.

Currently, the specification source code feeds into two outputs: a machine-readable code for proof checking and conformance testing, and a human-readable document for understanding. This issue is about the human-readable document.

## Levels of detail in human-readable document

The purpose of a formal specification is to define how a piece of software should behave. A specification needs to be human-readable so that humans can check that the specified behavior matches their intent. The key challenge is to present sufficient details to be unambiguous, while ommitting all details that hinder understanding. This challenge is hard.

A successful method for dealing with the key challenge is to build a tree of abstractions. An abstraction (such as "finite map" or "Token Algebra") at one level can be understood on its own, while the details of its implementation are presented one level deeper in the tree (such as "algebraic data types" or "finite map"). The key challenge is to be unambiguous without leaking details. For human-readability, a partial understanding at one level may suffice, as details can be looked up on demand by going into a deeper level.

In this spirit, I propose an organization of the human-readable output into "levels of detail". The idea is to group "specification code with prose" into a tree of abstractions that may improve human understanding. This proposal is only about the "code with prose" part, i.e. the formatting and style of the document — abstractions in the domain are entirely separate.

Given a function, such as `createRUpd`, the following groupings appear useful to me:

* "description" — high-level description of what the function achieves.
* "definitions, description" — high-level description of some arguments or local definitions in the function. In a programming language, these would be written as comments co-located with identifiers. In the ledger specification, I use `itemization` for this, as this keeps the precise definition tight.
* "definitions, abbreviated" — local definitions, but abbreviated notation such as `+` using type class magic.
* "definitions, full" — local definitions, in precise notation such as `ℚ.+`. Arguably, Agda's implicit parameters and type classes are an in-language way to trade between the "full" and the "abbreviated" level of detail, but it's not possible to have both. Perhaps on-hover-mouse could show type signatures?
* "proofs, full" — also show proofs. For the purpose of a specification, humans never need to look at proofs, as the compiler checks them for us; looking at the statements should be sufficient.

Navigation between these levels of details could be done through hypertext, e.g. hyperlinks, or "reveal / hide on mouse click".

For the "definitions, description" level of detail, the distinction between __usage site__ and __definition site__ came up. For example, the function `÷₀` is defined at the beginning of the specification, far away from its usage site in, say `createRUpd`. To aid understanding locally, the description of `÷₀` could be repeated at the usage site, but a hyperlink to the definition site of `÷₀` would also help with navigation, at the expense of nonlinear reading.

I suppose that "hyperlinking usage sites to their definitions" is a well-defined feature request, whereas I'm less clear on the "levels of detail". However, for the general problem of writing software that we can understand and verify, organizing the "levels of detail" effectively, be it through a formal specification or in code, is the key challenge.

Start by reading the thread in #752 and this issue's discussion of human-readable output, levels of detail, and hyperlinking usage sites to definitions. No source files, tests, or implementation entry points are named, and the issue does not define a concrete acceptance condition; a clear design and scope would be needed before work can be considered done.

Written by the indexing model from the issue text.