Axiom musings...

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Axiom musings...

Tim Daly
I have been programming for 50 years. There is always the
personal challenge of "keeping up with the edge".

In the wire-board and punched card days it was the ability
to choose the optimal sort for your data (almost everything
involved sorting).

Then came the cpu optimizations... write self-modifying code
that fit into the 64 byte cache. Or pick specially chosen chebyshev
values optimized for your sin function. Or do function-maps using
the Translate-and-Test instruction. Or micro-coding your loops to
enhance the CPU microcode for your program.

Then it was CMOS ASICs and FPGAs so your 16-bit multiplies
could REALLY pipeline.

Then PASCAL showed up and you weren't leading-edge if
you didn't do types.

and so on...

Now you're not even in the game if you aren't at least doing
$F_\omega$. (see Lambda: The Ultimate Sublanguage)
https://dl.acm.org/ft_gateway.cfm?id=3342713&ftid=2076175&dwn=1&CFID=149744317&CFTOKEN=2f53f2232d5db617-85952791-F402-7A5C-37FE69F835BDD124

It's what all the leading-edge kids are learning in school.

Next week you're behind the times if you aren't proving your
programs correct. You think your code "works"? Prove it.

And in two weeks you need to be using $\lambda{}C$.

Oh, wait... I'm already behind the edge.

All of this learning is time consuming and painful. But when
the Boeing plane crashes and the Airbus plane loses its
fly-by-wire and the Arianne rocket blows up and the Therac-25
kills patients and the Uber runs down pedistrians and the
facial-recognition AI system sends you to jail...It is time
to get serious about correct programs.

Since Axiom is computational mathematics it seems to
be a good place to start.

Tim

"it takes all the running you can do, to keep in the same place.
If you want to get somewhere else, you must run at least twice as fast as that"
-- The Red Queen in Through the Looking Glass"

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Tim Daly
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.

Tim





On 8/4/19, Tim Daly <[hidden email]> wrote:

> I have been programming for 50 years. There is always the
> personal challenge of "keeping up with the edge".
>
> In the wire-board and punched card days it was the ability
> to choose the optimal sort for your data (almost everything
> involved sorting).
>
> Then came the cpu optimizations... write self-modifying code
> that fit into the 64 byte cache. Or pick specially chosen chebyshev
> values optimized for your sin function. Or do function-maps using
> the Translate-and-Test instruction. Or micro-coding your loops to
> enhance the CPU microcode for your program.
>
> Then it was CMOS ASICs and FPGAs so your 16-bit multiplies
> could REALLY pipeline.
>
> Then PASCAL showed up and you weren't leading-edge if
> you didn't do types.
>
> and so on...
>
> Now you're not even in the game if you aren't at least doing
> $F_\omega$. (see Lambda: The Ultimate Sublanguage)
> https://dl.acm.org/ft_gateway.cfm?id=3342713&ftid=2076175&dwn=1&CFID=149744317&CFTOKEN=2f53f2232d5db617-85952791-F402-7A5C-37FE69F835BDD124
>
> It's what all the leading-edge kids are learning in school.
>
> Next week you're behind the times if you aren't proving your
> programs correct. You think your code "works"? Prove it.
>
> And in two weeks you need to be using $\lambda{}C$.
>
> Oh, wait... I'm already behind the edge.
>
> All of this learning is time consuming and painful. But when
> the Boeing plane crashes and the Airbus plane loses its
> fly-by-wire and the Arianne rocket blows up and the Therac-25
> kills patients and the Uber runs down pedistrians and the
> facial-recognition AI system sends you to jail...It is time
> to get serious about correct programs.
>
> Since Axiom is computational mathematics it seems to
> be a good place to start.
>
> Tim
>
> "it takes all the running you can do, to keep in the same place.
> If you want to get somewhere else, you must run at least twice as fast as
> that"
> -- The Red Queen in Through the Looking Glass"
>

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Axiom musings...

Clifford Yapp

On Sun, Aug 18, 2019 at 8:08 AM Tim Daly <[hidden email]> 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

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> wrote:

> On Sun, Aug 18, 2019 at 8:08 AM Tim Daly <[hidden email]> 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
>

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 <[hidden email]> wrote:
>> On Sun, Aug 18, 2019 at 8:08 AM Tim Daly <[hidden email]> 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
>>
>

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer