Re: [Axiom-developer] Axiom musings...

[Tim Daly]

Peter Naur addressed the primary issue of literate programming:
http://pages.cs.wisc.edu/~remzi/Naur.pdf

A "programming theory" is the ability to reason about a
program in some abstract sense. Given a question about
some theory of types (e.g. linear logic), you can close your
eyes and decide if it applies, how it applies, and how the
code either supports, or needs to be changed to support,
the use in question. You have a "theory" in your head.

This theory gives you the power to reason about the world.

It would be impossible to construct the theory from the
source code. That's what the literate programming form
is designed to fix. You explain what an "environment" is,
why it is needed, and why there might be several kinds,
as done in "Lisp in Small Pieces'. Then you include the
code to implement it.

To quote Naur:

  "For example, to have Newton's theory of mechanics as
  understood here, it is not enough to understand the central
  laws, such as that force equals mass times acceleration.
  In addition, the person having the theory must understand
  the manner in which the laws apply to certain aspects of
  reality, so as to recognize and apply the theory to certain
  other aspects. A person having Newton's theory of mechanics
  must understand how it applies to the motion of pendulums
  and the planets, and must be able to recognize similar
  phenomena in the world, so as to apply the mathematically
  expressed rules of the theory properly."

In your case, consider code to implement linear types. My
understanding is that linear types can be applied to things
like queues in distributed systems. A queue item is a use-once
item. Beyond that I haven't understood how to use this fact
and the theory to prove anything about a distributed process.

Literate programming is not about the code. It is about the
"theory" or "mental model". It addresses issues about the code.
It is, for instance, why I'm writing a section about "Why this
effort can't succeed", to address the theoretical questions that
seem to imply failure.

Teaching students to express their understanding of the model
gives them both a forum for showing what they understand and
a requirement to show that their code "covers" the model.

Don't confuse literate programming with "documentation" and
"comments".

Tim

On 8/19/19, Tim Daly <address@hidden> wrote:
> I sent my prior musings on Axiom and literate programming to several
> people, including several professors. One replied:
>
>   "Count me among the literate programming skeptics.  What
>    and where is a collection of examples that might demonstrate
>    its benefits?"
>
> So I thought it would be of interest to include the whole of the
> discussion from my side. (Since, as one researcher wrote,
> "I like reading opinions I agree with, especially ones I've written").
>
> The first part is the initial missive to the professors which
> generated the above reply. The second part is my reply to that.
>
> =============================================================
> PART 1: The email to the professors.
> =============================================================
>
> I have probably muttered to you about literate programming in the past.
>
> Like Lisp programming, it has the "enlightenment property". You don't
> "get it" until you "get it" and then you wonder why other people don't
> seem to "get it". It fundamentally changes everything about how
> you program.
>
> I've included my latest "musings" post below where I discuss the
> "intellectual space" that literate programs open. Why we don't teach
> this to the next generation is a mystery to me. We still teach students
> to develop programs in the POS (Pile of Sand) model, with all the
> "semantics" captured by 3 letter directory names "src", "doc", "tst".
>
> I wrote programs before the idea of directories was invented. I know
> it was invented as a "crutch". It is time to throw away the crutches,
> and at least stop insisting students use them.
>
> Like any other thing to learn, literate programming is painful to use
> for the first time. The "intellectual space" it opens is worth the
> experience.
>
> Consider requiring students to submit their homework problems in
> a literate program form. It will save them from the crutches.
>
> Tim
>
> As you might expect, the new Axiom Sane effort is fully literate,
> developed solely as a literate program.
>
> One of the subgoals is to write a page per day. This can involve
> explaining code. But it also involves explaining various ideas that
> are related to the effort.
>
> The current topic is a section on why this effort will fail. I have
> been looking for various arguments from people who give
> reasons why this effort cannot succeed.
>
> For example, Ron Pressler seems to think that writing software
> is beyond the difficulty of anything we've previously tried to do
> and that math (alone) won't help us.
> https://pron.github.io/posts/correctness-and-complexity
>
> Using fundamental results from Godel and Turing, Ron seems
> to show that software verification can't succeed. He may be
> right in the general case.
>
> Axiom isn't the general case. At least some of the algorithms
> encode mathematics, a small subset of the universe of Ron's
> argument and one where verification seems possible.
>
> The Sane effort targets verification of the GCD algorithms in
> Axiom. While this seems to be a trivial subset of Axiom with
> a reasonably clear specification the effort is not trivial. The
> overall goal involves restructuing Axiom so that the GCD
> specification, verification, and proof occur "naturally" because
> of design choices like inheriting axioms from Categories.
>
> I strongly  recommend trying to verify programs. There is a
> whole area of computational mathematics worth exploring.
> The benefit is a much deeper understanding of your code.
>
> In any case, it is certainly interesting to look for and write about
> reasons why this is impossible.
>
> It is also interesting to see the "intellectual space" opened up by
> literate programming. Besides the usual "documentation", it provides
> a space to discuss larger issues surrounding the problem to be solved.
>
> I strongly recommend literate programming. Any program has a
> lot of context, both with design ideas and supporting arguments.
> Literate programs give "space" to present these to the reader.
>
> And Axiom provides an "intellectual space" on the boundary between
> mathematics and general purpose code. If verification can succeed,
> Axiom is the ideal setting for experimentation.
>
> There is no such thing as a simple job.
> But this is certainly an interesting job.
>
> ==========================================================
> Part 2: My email reply to the skeptic response
> ==========================================================
>
> Lisp in Small Pieces by Queinnec explains lisp "from the bottom up"
> including the source for the compiler, interpreter, and debugger. He
> explains concepts like the environment in ever-increasing detail which
> makes the idea quite clear, for example. But not just the ideas as you
> can see, read, and understand the implementation details in code.
> https://www.amazon.com/Lisp-Small-Pieces-Christian-Queinnec/dp/0521545668
>
> Physically Based Rendering by Pharr and Humphrey explains the
> theory behind rendering, the geometry, the lighting models, etc. Each
> piece of code is associated with the explanation. This book is the
> "state of the art" of literate programming and is worth a look, even if
> you don't care about rendering.
> https://www.amazon.com/Physically-Based-Rendering-Theory-Implementation/dp/0128006455/ref=sr_1_2?crid=6ZPLOGT0PNRE&keywords=physically+based+rendering&qid=1566140907&s=books&sprefix=physically+based%2Cstripbooks%2C464&sr=1-2
>
> A very early version, without the hyperlinks, was John Lions' book
> "Lion's Commentary on UNIX 6th Edition", called the most photocopied
> book ever published (I have a second-generation photocopy). You could
> finally understand UNIX source code. I taught Operating Systems and
> have half a dozen books on the subject. I have the source code for the
> IBM VM and Burroughs 6600 operating systems, both of which are
> nearly unreadable without already understanding it. I was an IBM VM
> systems programmer and I still found it obscure.
>
> Lyon's book is still the best. Ken Thompson (UNIX author) wrote:
>     Finally- one of the most widely distributed underground computer
>     science documents is freely available. I can still vividly remember
>     the day in 1977 the first draft of these books came to me by mail.
>     I took a casual look expecting very little. I ended up reading every
>     word. After 20 years, this is still the best exposition of the workings
>     of a "real" operating system.
> https://www.amazon.com/Lions-Commentary-Unix-John/dp/1573980137/ref=sr_1_1?crid=5DCETY7XP4Y6&keywords=lions+commentary+on+unix&qid=1566141340&s=books&sprefix=Lions+Commentary+%2Cstripbooks%2C344&sr=1-1
>
>
> Think of a logic textbook. Cut out all the rules and past them on index
> cards.
> Give the students the index cards but not the surrounding explanations. It
> is
> unlikely that a student can understand the implications. This is the same
> thing
> we do with source code. We just give "the rules" but not the explanations.
>
> Or to give a more direct example, I am trying to understand the core logic
> in Lean. I would like to know the implementation of the rules. So I read
> the
> source code. The author is an excellent C++ programmer. His use of macros
> in data structures to implement reference counting is really elegant. It
> took
> me a long time to figure out what he was doing and why but I finally got
> it.
> The fact that I've published a paper in garbage collection helped a lot as
> I
> already had the background.
>
> However, after much effort I still cannot figure out which rules are
> implemented.  A simple paragraph surrounding each code block would
> give me a clue. But, instead, I am reduced to staring at obscure C++
> hackage.
>
> The long term implication of this nonsense is that the Lean system is
> unmaintainable once the author stops working on it. This happens all the
> time
> in open source. Github, Sourceforge, and Savannah have tens of thousands
> of open source programs that nobody uses because the initial author left
> and
> nobody can be bothered to reverse engineer the code pile.
>
> I was initially attracted to literate programming because I needed some way
> to make Axiom "maintainable" by someone other than me. It would be nearly
> impossible to swallow the 1.2 million lines of code (and the 3 comments)
> without some english language explanations. Nobody reads code that
> implements dependent type theory and just "gets it".
>
> Imagine how sweet it would be if your students could read a literate
> form of Standard ML, explaining and motivating the code and relating
> the code to the theory. How much nicer would it be if the ML type checker
> was something you could read and understand before lunch? Would a few
> paragraphs about the limits of the ML type checker inspire students to
> look for better algorithms? I suspect that not a single student has
> any clue about the internals and issues of Standard ML.
>
> Words. Communication with Humans, and as a side-effect, communicating
> with the machine. It changes everything.
>
> Consider it from a different angle, as if you're a prof in computer
> science.  You have a hundred books on your shelf. There are dozens of
> profs in the building, each with hundreds of books. Try to find one
> who has a program listing on their shelf (I have a dozen).
>
> What is truly amazing is that profs don't even have a listing of
> their PhD thesis on the shelf. I've contacted 1/2 dozen or so to
> get a copy of their PhD thesis code. So far, nobody has shown
> me a copy, partially because they don't have it or they know that
> it won't run anymore. My machine vision code is gone (of course,
> so is the paper tape containing it, and the PDP 8).
>
> Source code dies. Books live. The ideas in books live. I have
> books on my shelf from Frege, Turing, and Kleene.
>
> Literate software lives. Even if it doesn't run it shows how it could.
> The code illustrates the ideas, like formulas in a calculus book.
>
> Consider how it can change teaching.
>
> In the simple case, require the assignments to be literate. Ask
> the student to explain how Cut works and its use in a proof.
> Some bright spot in class will come up with a really clear
> explanation you can probably use in a textbook.
>
> You can ask for a literate version of your proof checker program.
> Each student shows the rules and has to explain how the whole
> program works. It is trivial to copy code from someone but it is
> hard to copy the explanation. They can even work in the
> language of their choice since the explanation makes the ideas
> clear.
>
> You can assign a semester project, such as "Explain the
> lambda cube. Give literature references." Then instead of a
> final exam you can see who really understands it. See who
> notes that the left half is propositional logic and the right half is
> predicate logic. As a side-effect you introduce students to the
> literature.
>
> You can even have the students in this year read and improve
> code from last year. As the code base gets larger you can
> assign chapters, like the type checker or the parser chapter.
> Eventually you can use the literate form as the textbook.
>
> Literate software doesn't even impact your automation. Axiom
> uses a 170 line C program to extract code from documents.
> So you can run the code through your compiler or your code
> checker or whatever automation you use.
>
> If you really want to be "retro" you can use the Makefile to
> extract code from the literate sources and "recreate" the
> src, doc, txt POS structure. It is only one more stanza
> in the Makefile.
>
> Books live. They structure your thinking. People know how
> to use a book. They understand the chapter, section, and
> paragraph structure. They get the table of contents, index,
> list of tables, and bibliography. The new books can be fully
> hyperlinked, even to outside web sources.
>
> Literate programming literally changes the way you think
> about programming, even more profoundly than types.
>
> Teach your students to write code that lives.
>
>
>
>
> On 8/18/19, Clifford Yapp <address@hidden> wrote:
>> On Sun, Aug 18, 2019 at 8:08 AM Tim Daly <address@hidden> wrote:
>>
>>> For example, Ron Pressler seems to think that writing software
>>> is beyond the difficulty of anything we've previously tried to do
>>> and that math (alone) won't help us.
>>> https://pron.github.io/posts/correctness-and-complexity
>>>
>>> Using fundamental results from Godel and Turing, Ron seems
>>> to show that software verification can't succeed. He may be
>>> right in the general case.
>>>
>>
>> Thanks for that link - I had seen that video, but didn't know (or had
>> forgotten about) the write up.  I found that talk extremely interesting.
>> What it seems to make an excellent case for is that we're never going to
>> get to a point where we are bereft of practical challenges getting
>> computers to do what we want them to - the limitations of mathematics and
>> computers fundamentally preclude it when we tackle complex problems.
>> (Fortunately that doesn't mean it isn't worth attempting to get things
>> right anyway - it just lets us manage expectations both of people and
>> outcomes when we try.)
>>
>>
>>> Axiom isn't the general case. At least some of the algorithms
>>> encode mathematics, a small subset of the universe of Ron's
>>> argument and one where verification seems possible.
>>>
>>
>> That makes sense to me.  One of the takeaways for me from that talk was
>> *not* that all formal efforts are ultimately futile - only the attempts
>> to
>> completely eliminate all errors of any type.  Instead, the useful
>> activity
>> is to focus on applying such techniques to progressively eliminate the
>> more
>> probable failure modes (what he terms "common and costly bugs") observed
>> in
>> real world systems to improve the chances of successful user outcomes.
>>
>> Axiom is by design and intent focused on mathematics - i.e. that portion
>> of
>> the Venn diagram which is provable.  Because it must be a computer
>> program
>> running on a computer system there will always be some uncertainties (if
>> nothing else we are dependent on correct behavior of the hardware, which
>> is
>> subject to entropy over time) but the *exact* same thing is true of
>> humans.  What a Computer Algebra System can ultimately provide (in
>> theory)
>> is to exploit a computer's deterministic, reproducible information
>> manipulation to be more accurate than anything a human brain could
>> achieve
>> on its own, and that is of immense practical value.  The running (indeed
>> infinite) challenge is to see how low failure rates can be pushed
>> practically, and formal systems provide a framework within which to do
>> that
>> pushing.
>>
>> CY
>>
>