[Axiom-developer] Literate Programming

[daly]

An extended quote from:

Mills, Bruce "Theoretical Introduction to Programming"
Springer-Verlag 2006 ISBN 1-84628-021-4 pp 10-11

Notion 5: Literate Programming

Donald Knuth once said,
... when you write a program
      think of it primarily as a work of literature.

To program in computing is to prove in mathematics: both in syntax and
in semantics. The formal structure of a program is identical to that
of a formal constructive proof. To write a routine is to assert the
theorem that {\sl the code performs to specification}.

Although there are errors in mathematics works, the density is much
lower than in contemporary programs. In the mythos, this is due to a
greater complexity or urgency of software. The truth is, mathematics
was designed to be understood. A mathematics book does not just prove,
it also motivates, justifies, and discusses. This human nature makes
it easier to follow, detect errors, use elsewhere, or extend.

The larger part of the life of a piece of software is maintenance. The
code is modified to suit new specifications, conceptual errors are
identified and corrected, and typographical faults removed. This is
also the life of a mathematical proof.

A mathematical proof can be lengthy, technical, complex, obscure and
urgent: and yet it will not be left without justification. The
mathematical community would not accept it if it was. The fact that
much code is written without proper contemplation today is related to
market forces.  But, whatever excuse we give for why there is this
lack, this means (very) low-quality code.

There are good proofs and there are bad proofs. A good proof conforms
to both logic and intuition. A bad proof might give no clear concept
of why the result is true or might be difficult to follow. A flawed
proof with good discussion may be of more use in the development of
related correct material, than a technically correct proof with no
explanation.

Code should be written to be clear by itself, but also with good
comments.  More than just a cursive phrase stating {\sl this variable
stores the number of hobos found in Arkansas}. It should contain
discussion, explanation, and justification.

The natural language in a mathematics book is like the comments in a
program and is typically more extensive than the formal language. We
can compute $f(n) = \sum_{i=1)^n{i}$, by a loop. The loop is
``self-commenting'' because it reflects the original specification.
But it is better to compute this as $f(n)=n(n+1)/2$ relying on the
identity $f(n) = \sum_{i=1)^n{i} = n(n+1)/2$, which is by no means
obvious. In the code, we need a non-trivial comment to explain why
what we are doing works.

A program should be developed with a coherent theory of its operation.
Clearly defined data structures, with explicit axioms, greatly ease
the use and re-use of the code. If each item has a clearly explained
purpose and a distinct, justified, and discussed property, if each
item is a whole as well as a part, then it is much less likely that a
later programmer will accidently misuse it.

Consider a program to be written primarily to explain to another human
what it is that we want the computer to do, how it is to happen, and
why we can believe that we have achieved our aim. Do this even if you
write code for yourself. The ``other'' human being might be you in a
few month's time when the details have escaped your mind.

I have found it advisable that, in selecting what to write in comments,
if you have just spent a lot of time writing a routine, you should
write down what is obvious. Because it is likely that it is only
obvious to you now because you are steeped in the problem, next day,
next week, or next month, when you come back to modify it, the
operating principle might not be obvious at all.

Literate Haskell style is supported by typical Haskell environments. 
In this approach, the code-comment relation is reversed. Normally the 
code has primacy, and the comments are introduced by a special syntax, 
as if in afterthought. In the literate approach, the comments are 
primary.  By default, text is comment; the code must be introduced by 
a special notation stating that it is code.




and another comment from the same book: p346

There are several concepts wrapped up in the idea of literate
programming.  However, the central matter that I am interested in here
is that programming by humans should be a human enterprise. Knuth has
suggested that a program should, first and foremost, be a literary
work, to be read by humans. This is analogous to the approach in a
mathematics book.  The text of the book is like the comments in a
program, and it is typically bigger than the formal development.


Tim