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 |
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 |
On Sun, Aug 18, 2019 at 8:08 AM Tim Daly <[hidden email]> wrote: For example, Ron Pressler seems to think that writing software 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 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 |
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 |
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 |
Free forum by Nabble | Edit this page |