Literate Programming in the Large

I like Tim Daly's viewpoint that we shouldn't just be writing code , but we should write manuals - giving high level overviews of our problems and specifying their implementation details inside the manuals. His talk "Literate Programming in the Large"[1] covers why. The example he gives in his talk is the Axiom algebra system[2], which was revised to use literate programming style - the source code, with usage examples, is contained entirely within the books. [1]: [VIDEO] , [sldes]: [LINK] [2]: [LINK]

I've been using literate programming for 15 years on many projects. The largest and most visible one is Axiom ( [LINK] ) which currently has many thousands of pages with embedded code. I've talked to Knuth. He claims he could not have implemented MMIX without literate programming. Literate programming is really valuable but you only understand that once you really try it. I gave a talk on this subject at the WriteTheDocs conference: [VIDEO] You can write a literate program in any language, for instance, in HTML: [LINK] There are some "gold standard" literate programs: "Physically Based Rendering" by Pharr and Humphreys won an academy award. "Lisp in Small Pieces" contains a complete lisp implementation including the interpreter and compiler. The book "Implementing Elliptic Curve Cryptography" is another example. Suppose your business depends on a program. Suppose your team leaves (they all do eventually). Suppose you need to change it... THAT's why you need literate programming. Nobody is going be around to remember that the strange block of code is there to handle Palm Pilots. Companies should hire language majors, make them Editor-in-Chief, and put them on every programming team. Nobody checks in code until there is at least a paragraph that explains WHY this code was written. Anybody can figure out WHAT it does but reverse-engineering WHY it does it can be hard. Imagine a physics textbook that was "just the equations" without any surrounding text. That's the way we write c

I think there are two sound approaches to communicating complex systems between humans (which is the main goal here, a computer might be a bit slow compiling 200M LOC - but the real problem is that no human can read that much code, let alone understand it): 1) Write documentation that is also code. That is the idea of literate programming. I recently came across: "Literate Programming in the Large": [VIDEO] which is a bit of a wandering talk, but well worth watching: it talks about real, huge comolex systems, and how lp can help bring them back under control. 2) The other approach is to shift your perspective, so you don't have a complex solution to a compkex problem; but rather a few small and lightly connected straight forward solutions to simple problems. Now I doesn't matter if you're bad at communicating, because the ideas you try to convey are simple ideas. I think there are a few reason that STEPS appear to work: what we're doing with our complex software is simple stuff. If we know what we want to do (the hard part) doing so in a straightforward way becomes easy. If we can make hierarchies of abstraction and isolated sub-systems. Note that simple doesn't mean trivial. These solution often require quite a lot of theoretical education; but not an unreasonable amount.

I found this talk about re-structuring and bringing back to life a 1.2 MLOC lisp codebase with classical LP interesting (it's a bit meandering, but INHO well worth a watch): "Literate Programming in the Large": [VIDEO] The reorganization is still ongoing, as can been seen at: [LINK]

There's a (somewhat rambling, but interesting) talk on the effort to rewrite the lisp symbolic math system Axiom[a] as a literate program (spanning several books) - precisely in order to make it possible to refactor and maintain the code: "Literate Programming in the Large": [VIDEO] [a] [LINK]

"Programs should be written for people to read, and only incidentally for machines to execute." (Structure and Interpretation of Computer Programs" by Abelson and Sussman) The idea is that you write a "Book" and the program is extracted, from the book. Literate Programming Wikipedia: [LINK] A nice talk about it: [VIDEO]

You wrote "There's a fundamental problem with generating a beautifully typeset document for a codebase: it's dead. It can't render inside just about any actual programming environment (editor or IDE) on this planet, and so we can't make changes to it while we work on the codebase." Sorry, that's not correct. When writing a literate program you should also include a chunk containing a Makefile. Extract the Makefile and let it construct the program. I did this with the whole Clojure programming language. The whole source code for all of Clojure, as well as the test cases, are in the PDF. The sequence (from scratch is): Extract the Makefile from the Latex document. Run the Makefile. This: 1) extracts the code and tests 2) compiles the code 3) runs the tests 4) recreates the PDF from the Latex So you edit the Latex text and/or code with any editor and then re-run the Makefile. This will rebuild your program, runs the tests, and re-makes the PDF. If you have the PDF open next to your editor it is likely that the PDF viewer will reload the changes immediately. This ensures that (a) your program compiles, (b) your program passes tests, and (c) the PDF builds correctly. I've been working on literate programs for years. See [LINK] . I've even given a talk on the subject See [VIDEO] ). I find literate programming to be the MOST important change in programming since I started in 1970.

Thanks for the "all the work" complement. Despite all, it is more fun than work. Computer algebra algorithms are basically functions. Axiom is unique in that it organizes the functions based on a group theory scaffold. Thus you can know that certain matrices commute but rectangular ones don't. Algorithms that know how to commute live in the commutative "category" in Axiom. So the game is to distribute LEAN's commutative axioms in their proper place in the group theory inheritance scaffold so they are available when they apply. Axiom arranges the world into "categories" (not category theory stuff) and "domains". The LEAN structure is a third structure (actually fourth but...) built in parallel so that a theorem that proves that certain matrices commute will only be available when it applies. When you try to prove your algorithm you have a collection of LEAN axioms, definitions, and tactics that are valid and apply to your particular function. If your algorithm used rectangular matrices the commutative theorems would not be visible and thus not available in a proof step. Due to the hierarchical nature, once you prove an algorithm you can also use it in other downstream proofs, for example, using proven data structures and their properties. I have not published any papers on the subject. I'm no longer anywhere in the academic pipeline so a paper wouldn't get very far. Plus this is "in the cracks" kind of research that doesn't seem to fit into either camp. As for the education or