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

[Tim Daly]

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
>