From MAILER-DAEMON Sun Aug 04 14:02:45 2019 Received: from list by lists.gnu.org with archive (Exim 4.86_2) id 1huKqD-0006hj-9t for mharc-axiom-developer@gnu.org; Sun, 04 Aug 2019 14:02:45 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:41549) by lists.gnu.org with esmtp (Exim 4.86_2) (envelope-from ) id 1huKqB-0006hc-Bi for axiom-developer@nongnu.org; Sun, 04 Aug 2019 14:02:44 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1huKqA-0008Pm-A1 for axiom-developer@nongnu.org; Sun, 04 Aug 2019 14:02:43 -0400 Received: from mail-lj1-x234.google.com ([2a00:1450:4864:20::234]:32972) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1huKq9-0008OX-W3 for axiom-developer@nongnu.org; Sun, 04 Aug 2019 14:02:42 -0400 Received: by mail-lj1-x234.google.com with SMTP id h10so5827160ljg.0 for ; Sun, 04 Aug 2019 11:02:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=cGnEqPgA9r5utFXUKriHlU9zSaj9TQxiO6yzTqpzykE=; b=RDfpWrQDTk3nyoA2vrPiKZhViP2tOt9msSlQE1Z+z1VZbiJzWgihI0Y25P3FFm21Ef yOeDFKj7ltxKVuRTuJJefQpHJpmOdzKU7E0YowK+Rx3UiWTeQQzcAZ/n4y5I30/xDHzo Z17MQ6CB1OOJc3WsZkQ3PHMbA0XdRS0Yekhj60/0mAoqoMmk2MXv5qJUWtJjHWcOO9WM E7QsoYXyhn25Texqy1Bd/dbayqgDgKwiX3qkNWat5gXAbQeNmAALwis14vzYTot32umf 5t5AzcU//j/gvAAFcgJEllQT7PlHnClQ1ZMsdzkZ5aLuqkA/FkaiEAlc3QBuhT7833bM bHrw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=cGnEqPgA9r5utFXUKriHlU9zSaj9TQxiO6yzTqpzykE=; b=slpf2mkWxRC6QZ8BjonhANzSXXx1n5yllfU4jVLDoKGgtV/21EtqRdg53hr4e4mzwU jgn5N3XSSkp0gJ8mM6tksnQuv5yWKgUQ88wuIdRkbS8nC/3RUkHb1uupY5VOsvyTPQyr lHku0B7GbdsPFITIjdv2MJ9+LS+kQBBcSTr2mLY3+uxIMPV+fgwO8NfQdYnkEB1ao++P 6VR0cxNBMCI6H0n6/MG0N6M1/ALDiRDtGGVhlrvqweH6wrQ6Td6GaNkPOLM1oTln68d2 3KdzX1y0wUoZ/jYaXFAr9niwWkDaxu62s5ShcGBaXL04tvySFXHhd07RQ8R3qUV750uB JCRA== X-Gm-Message-State: APjAAAV81PBmbLxWtjkmYedycjsloRHNcbvELo3T1DW4BO0r5Q8XYIz9 3u4ts1V7SylIUurpkt/u5DUmul4fIh3/b0CfOkBAVwAr X-Google-Smtp-Source: APXvYqxVrHogF0Msir9H9XovEGJurPNG29nQOqi5ViRFYmxIyquUpY34jY0c8RdK5N7bEUT9x2lBKJtGw/pmu5c0QPs= X-Received: by 2002:a2e:12c8:: with SMTP id 69mr74686221ljs.189.1564941759212; Sun, 04 Aug 2019 11:02:39 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:ab3:5e04:0:0:0:0:0 with HTTP; Sun, 4 Aug 2019 11:02:38 -0700 (PDT) From: Tim Daly Date: Sun, 4 Aug 2019 14:02:38 -0400 Message-ID: To: axiom-developer@nongnu.org, Tim Daly Content-Type: text/plain; charset="UTF-8" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::234 Subject: [Axiom-developer] Axiom musings... X-BeenThere: axiom-developer@nongnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Axiom Developers List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 04 Aug 2019 18:02:44 -0000 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" From MAILER-DAEMON Sun Aug 18 08:08:26 2019 Received: from list by lists.gnu.org with archive (Exim 4.90_1) id 1hzJz0-0007Sz-Cr for mharc-axiom-developer@gnu.org; Sun, 18 Aug 2019 08:08:26 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:42558) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1hzJyx-0007Qu-TQ for axiom-developer@nongnu.org; Sun, 18 Aug 2019 08:08:25 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hzJyw-0006Ak-Cv for axiom-developer@nongnu.org; Sun, 18 Aug 2019 08:08:23 -0400 Received: from mail-lj1-x234.google.com ([2a00:1450:4864:20::234]:35309) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1hzJyw-00069k-3Q for axiom-developer@nongnu.org; Sun, 18 Aug 2019 08:08:22 -0400 Received: by mail-lj1-x234.google.com with SMTP id l14so9069256lje.2 for ; Sun, 18 Aug 2019 05:08:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=o6fkrcX//GLr/IqAvPdSuzKnJgaFMyttii8GL1RpP0o=; b=ffwCxAc4+ErdCdZzj/NonppW8u6oi9T9Z7oh1DjNJblyA64GAAaJtG5jEOZewnLm/K aSeJlcd/S7hECdoRljAR+3qunlu7MJmF4sfZ0lpVahzl4J9wNNGXUs/WLUsnFBmRIcuy P8t9lAT6i58JwsB9X4O9z9zRvSnF108Dq4qpA23T8iEnYJM2w0OeV8fQLZvvvBBX4Vpl n8uAaeUvkeOGSXAYUBrYiPyLVCNgYgd7qTm2DfaRrImC5sjxDDRu3R7J6vaXs+rvQSxB Uw7NnxwBuKF6wWK1lX4lNJHvRGBSXwa6l6Rv6hSi7MNRlhJVSQHeuutTi6038ZlQPgth 1rWQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to; bh=o6fkrcX//GLr/IqAvPdSuzKnJgaFMyttii8GL1RpP0o=; b=JVbOkmf0ayelvjGbPbk1zo6gvtZmvmaAMMGERNsXfztzZdd862VGjjT2ORYJ7JLzGg NV3bIRrRKitEF/ybCAUOPfDPS/iUEXLD7qxm1Wiyh25f69sazCluJPjQ2Eps5XZEPps6 8K7wdu1/j9bEipZb1sBQwCz+gWInRwwxqVAH8Ik+eSjGd97Sj275ZZfswdp+P4dc5k+H BEnLwDBUQOOb3GhnNDiwl9uK3ArILpNcPY3z/Ff9wE0Ob3A8osindmj9sEVuroJS76qC pzOw3NL4mvaRFuOj+t0Mw2WOepr4y8SoCSO1YM9moSFKY6UNZ1HKHLfFLcjHK5BCqYYz rbrQ== X-Gm-Message-State: APjAAAVj0K8wuFqmlRGEfrBcGS2HjaatPFfNgPshKRzCqGIyBGStYWmw 1TSpB1xl9VbuSCKoCjKwsiuFN/JNZr9knYlPPel8jQ== X-Google-Smtp-Source: APXvYqwq49Ipf9AIAmW0cSSeqC9klIMYEFZ43m2FH7qpbloRDjc8mKJNRqs5PXLqyx3XC0h4SAKSNUW8ggn0dbi7ZZ4= X-Received: by 2002:a2e:5c5:: with SMTP id 188mr10238963ljf.166.1566130099567; Sun, 18 Aug 2019 05:08:19 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:ab3:fcb:0:0:0:0:0 with HTTP; Sun, 18 Aug 2019 05:08:18 -0700 (PDT) In-Reply-To: References: From: Tim Daly Date: Sun, 18 Aug 2019 08:08:18 -0400 Message-ID: To: axiom-developer@nongnu.org, Tim Daly Content-Type: text/plain; charset="UTF-8" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::234 Subject: Re: [Axiom-developer] Axiom musings... X-BeenThere: axiom-developer@nongnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Axiom Developers List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Aug 2019 12:08:25 -0000 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 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" > From MAILER-DAEMON Sun Aug 18 11:10:10 2019 Received: from list by lists.gnu.org with archive (Exim 4.90_1) id 1hzMos-0003D2-Qf for mharc-axiom-developer@gnu.org; Sun, 18 Aug 2019 11:10:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:58820) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1hzMop-0003Cc-UY for axiom-developer@nongnu.org; Sun, 18 Aug 2019 11:10:09 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hzMoo-0005gR-Ai for axiom-developer@nongnu.org; Sun, 18 Aug 2019 11:10:07 -0400 Received: from mail-qt1-x82a.google.com ([2607:f8b0:4864:20::82a]:37783) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1hzMoo-0005g4-5e for axiom-developer@nongnu.org; Sun, 18 Aug 2019 11:10:06 -0400 Received: by mail-qt1-x82a.google.com with SMTP id y26so11435907qto.4 for ; Sun, 18 Aug 2019 08:10:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=SPZyupe97nbI64HATkr8sbl+JrNxncVpwc/yG4nsXBc=; b=nuNoIhAmA6QGgXWLsv1JeQN+S56i9NzcaXTceg8hi6O0khYd1hivnYdtcsjGAEOwAN 7/a5Wx0NqkFETnItruqvI4eJV5n1JjlG98a/08Vr905p+AWg77SMxqs7tiYyZxcwlzHm FrVsJxI0YwX2zNaTJezDEYe0L8C/71CHo4vax8qQeyXqBUgSEL8r7cVJNbJpa+y69Zhu Yz+3qcjoiCMKH00wctkKJqb+6a3aFREOb7rUQcDrBszI+gnQL8//jvYu2EzERJooHegX ZRlcsCIl/mPx+Eti6fmRIfHOw8jFDIA/0xGI3PbCHE9BRp+yLdDwZf6gY9ZFla1IzSKc U/AQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=SPZyupe97nbI64HATkr8sbl+JrNxncVpwc/yG4nsXBc=; b=M61xYaDRcXbp4z8d7KW1AW9bnZLWcU69VI+qGRNNv7t/xIwpIgzmYb3eYUwEbLou8H dTMRSO9owvdy4Nhwma1gkNxFQDKnEzu/ZS1xsNV2g8AMw4XoQrVGochvbn5omm6Z9U0C Yn+ybY+RwMAiUIVE/OhY5H3BdOQALu3PdlvYP0Zq3BesmTXkhtrPH9ayZod9WKEOg79I wTK3ELEyBxvBr/4nU3G/cgO/rtrUA7qvxSDSgvYXUQ8LbtuTCB6wT/8tgPNB8exKOfR4 CAF8z0xH4TgSWV2VNYcSfxP5/3uLGe6+8Z39sJuhQrEFRiwY9BQnsDUwpP4hk1jjqMg2 sb/Q== X-Gm-Message-State: APjAAAWPDLQQE1eKWth9aobhF3o3fKneSk78v2omCM/m3PMBQfdzEh5N mPkeComOqk5PVPP8DqTCOrxna88xDsjSUoZ7JB0= X-Google-Smtp-Source: APXvYqxIgA5ftOW4TDPspLr8TU8PMVpdYk2x15X25rVkKD00bOb60k6Y1O6AlO23SP4RJ1w6MK2Um2mahOTKQXNVTro= X-Received: by 2002:ad4:50d1:: with SMTP id e17mr8169618qvq.9.1566141004702; Sun, 18 Aug 2019 08:10:04 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Clifford Yapp Date: Sun, 18 Aug 2019 11:09:53 -0400 Message-ID: To: Tim Daly Cc: axiom-dev Content-Type: multipart/alternative; boundary="00000000000040e5cd0590659ebb" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2607:f8b0:4864:20::82a Subject: Re: [Axiom-developer] Axiom musings... X-BeenThere: axiom-developer@nongnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Axiom Developers List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Sun, 18 Aug 2019 15:10:09 -0000 --00000000000040e5cd0590659ebb Content-Type: text/plain; charset="UTF-8" On Sun, Aug 18, 2019 at 8:08 AM Tim Daly 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 --00000000000040e5cd0590659ebb Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

On Sun, Aug 18, 2019 at 8:08 AM Tim Daly <axiomcas@gmail.com> wrote:
For example, Ron Pressler seems to thi= nk 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 t= hat link - I had seen that video, but didn't know (or had forgotten abo= ut) the write up.=C2=A0 I found that talk extremely interesting.=C2=A0 What= it seems to make an excellent case for is that we're never going to ge= t 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 f= undamentally preclude it when we tackle complex problems.=C2=A0 (Fortunatel= y that doesn't mean it isn't worth attempting to get things right a= nyway - it just lets us manage expectations both of people and outcomes whe= n we try.)
=C2=A0
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.=C2=A0 One of the takeaways for me from= that talk was *not* that all formal efforts are ultimately futile - only t= he attempts to completely eliminate all errors of any type.=C2=A0 Instead, = the useful activity is to focus on applying such techniques to progressivel= y eliminate the more probable failure modes (what he terms "common and= costly bugs") observed in real world systems to improve the chances o= f successful user outcomes.

Axiom is by design and= intent focused on mathematics - i.e. that portion of the Venn diagram whic= h is provable.=C2=A0 Because it must be a computer program running on a com= puter system there will always be some uncertainties (if nothing else we ar= e dependent on correct behavior of the hardware, which is subject to entrop= y over time) but the *exact* same thing is true of humans.=C2=A0 What a Com= puter Algebra System can ultimately provide (in theory) is to exploit a com= puter'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.=C2=A0 The running (indeed infinite) challenge = is to see how low failure rates can be pushed practically, and formal syste= ms provide a framework within which to do that pushing.
=C2= =A0
CY
--00000000000040e5cd0590659ebb-- From MAILER-DAEMON Mon Aug 19 09:13:10 2019 Received: from list by lists.gnu.org with archive (Exim 4.90_1) id 1hzhTC-0008N1-Ov for mharc-axiom-developer@gnu.org; Mon, 19 Aug 2019 09:13:10 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:50383) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1hzhT4-0008IW-0G for axiom-developer@nongnu.org; Mon, 19 Aug 2019 09:13:05 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hzhSz-00017w-4L for axiom-developer@nongnu.org; Mon, 19 Aug 2019 09:13:01 -0400 Received: from mail-lj1-x243.google.com ([2a00:1450:4864:20::243]:33455) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1hzhSg-0000yh-Pr for axiom-developer@nongnu.org; Mon, 19 Aug 2019 09:12:51 -0400 Received: by mail-lj1-x243.google.com with SMTP id z17so1723123ljz.0 for ; Mon, 19 Aug 2019 06:12:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=6xYe6sc1h715xKLVNXmGxA5tCoZ3BT7IJrxI1PrHTzs=; b=gerv8uTfzjpdqLOF9dLam6BRC9i4GnqVn9iCJR5CDvnwK33Ko2YR9nnbbpx37q3utu rju0xD8T1Z2rYq9yhMzYjKgqOySZzk9/xV/iz7EqkWFEB1a59aJhnCn5HFqNl+Og60qK LUrspJtrqqCTwFwscvVjoIRFg6u6SAeQY0dSUUJfBQFbzv7K3bvZdooVkVzJowT+P4ZN RMrkSrktW41kGEB0gXGM7lxWTspVc2qyDdVU64WxC6a8zUn9L9GQvIqlzSC5/saCRA4H UFlaDByN0VRzDrXBD+C9x8T6eBEhBksdSXVD8FSlpeKW0S70OgrTqGbq4UqqbDAAYdVg y3qw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=6xYe6sc1h715xKLVNXmGxA5tCoZ3BT7IJrxI1PrHTzs=; b=kNgDs9QLd83nKobRycIeEy3lpnHrAfVQuZ/Pbp2uQK0tXUUqa9DCIlCdlhmQDQc0J1 7ILr3YVQZTTdB62KeNlE+nWPF08ry0t8NEgvfA4LkSv65XwcdBmRQBdkyh+ljI/GaslC SAVFQqOuaBlndst0/wdXvsXJL25d1i0ykrraqGfelHOxJmlhrR9MZjmrB4X7CciQlFEg RylVG4c5jYydnt4GIJZPC1mOHinsqNcOWl9EmmFq5iczJVYUCM2/6q1Y7FZgUEq/oDzt qciIMfIthKF2cco16C87rZNFIXbHoHdRGMO1v8XIK8peCVSjz6NV/uU9qs7eAQm2a1qG BYIQ== X-Gm-Message-State: APjAAAX9GFiVYZ3ST2PUfSOsk5+w1LLCQa/1R58KRRsBvQmNVukC/fpq MdTanVye3Ofb4te4ACMQiB7q9csBqb7/voNQzjE= X-Google-Smtp-Source: APXvYqy8qhBoJhih9711DH9UksksYrIrXJ+1IbBgVzoCkkXqz6ejJJTv6W6ShfB2w1WHuarQ9PjrdGJV5SAZe1fHbl8= X-Received: by 2002:a05:651c:158:: with SMTP id c24mr8353501ljd.66.1566220355225; Mon, 19 Aug 2019 06:12:35 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:ab3:fcb:0:0:0:0:0 with HTTP; Mon, 19 Aug 2019 06:12:33 -0700 (PDT) In-Reply-To: References: From: Tim Daly Date: Mon, 19 Aug 2019 09:12:33 -0400 Message-ID: To: Clifford Yapp Cc: axiom-dev Content-Type: text/plain; charset="UTF-8" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::243 Subject: Re: [Axiom-developer] Axiom musings... X-BeenThere: axiom-developer@nongnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Axiom Developers List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 19 Aug 2019 13:13:05 -0000 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 wrote: > On Sun, Aug 18, 2019 at 8:08 AM Tim Daly 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 > From MAILER-DAEMON Tue Aug 20 16:02:09 2019 Received: from list by lists.gnu.org with archive (Exim 4.90_1) id 1i0AKX-0004TH-BI for mharc-axiom-developer@gnu.org; Tue, 20 Aug 2019 16:02:09 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:44705) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1i0AKS-0004RU-7r for axiom-developer@nongnu.org; Tue, 20 Aug 2019 16:02:06 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1i0AKP-0006RR-Ip for axiom-developer@nongnu.org; Tue, 20 Aug 2019 16:02:04 -0400 Received: from mail-lj1-x242.google.com ([2a00:1450:4864:20::242]:46513) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1i0AKP-0006MA-38 for axiom-developer@nongnu.org; Tue, 20 Aug 2019 16:02:01 -0400 Received: by mail-lj1-x242.google.com with SMTP id f9so6288521ljc.13 for ; Tue, 20 Aug 2019 13:01:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=Z3ZGRf/J+JQ9MSiP/rYVf3fy4JK5KuA4Fk+1sK2cY+E=; b=kVPZ/lsHPnojw54K3VcKmPH5G1PtmlEA5R2ZtABMtUqirQf/zuFMjoU7fNGTqGdNxb aml8fDEPD2Yd/rjkRm0/rZB23fSWg9MZkwWVVwwxMzZbL9NgV2IjgCwqLmHihy5PGGon NIXohH0JHg+ibQb1yR7jaULFSsUrjHIFEJ/n/mdSjYulStF+15m+Ks3YMPLDrMMWfa9b k9m1lY8vTEUs0/mziFnIpBIu4NPB4rtDHvoD16Y6OMgikiDODCIZnhkRmur8Cz0Nfs7u vQLKEWYsCRW9+1jH8OjPqT+4t4ruOgHVZN3YYjis64c7eoToRfAV+oozzADLCRiTObc7 onoQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to; bh=Z3ZGRf/J+JQ9MSiP/rYVf3fy4JK5KuA4Fk+1sK2cY+E=; b=TWxCYxEh8xEt2+Eot/CL2Eh8BZr5HTPSTVY6GVGKp6J1pbzy6NNHvSvLbrV8ySiCGM 2CJuDjz1uwffjt4G7IBy7UQfOHPhPiMKn+RP11kAtiSCvEd/djfQhq+lhKqD0MHqBJoA ZoVFwzDNTEATHvPu71SbUw1oo4baB9Z9gEX42155myz/Tn18DidYMcb9xbD6geqCr3jk vAkXnXyu0KPuLumCCFfs4grctsBN0WasF51e917apFiir/9ut3aSFdNfWIIVIrZua5/9 xK+5Z3c5k2j5/ASnkDX/Y0yH5MYmK+WDYgP2oTmwr9JCoc00Opewpp5GxG4vvZlrr3Ph VMIw== X-Gm-Message-State: APjAAAU5xreyZ/6KQ80ZiVPPJMGDZwIjfJgJxi8V42FeLCI3oN2dISia n4SgAL0g4FWzrdD9nQVBy/4V2GVi0JUWwO2z93+XZQ== X-Google-Smtp-Source: APXvYqwaqfQdR0i7UGsjoRL21VUsA60Q5QqLNjOXy7t2/7kDXljbaEQ4wgm9Td2+DRZNv9/WIO16iHbL7UvMP4TmFiA= X-Received: by 2002:a2e:5c5:: with SMTP id 188mr1712336ljf.166.1566331305634; Tue, 20 Aug 2019 13:01:45 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:ab3:fcb:0:0:0:0:0 with HTTP; Tue, 20 Aug 2019 13:01:45 -0700 (PDT) In-Reply-To: References: From: Tim Daly Date: Tue, 20 Aug 2019 16:01:45 -0400 Message-ID: To: axiom-dev Content-Type: text/plain; charset="UTF-8" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::242 Subject: Re: [Axiom-developer] Axiom musings... X-BeenThere: axiom-developer@nongnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Axiom Developers List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 20 Aug 2019 20:02:07 -0000 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 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 wrote: >> On Sun, Aug 18, 2019 at 8:08 AM Tim Daly 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 >> > From MAILER-DAEMON Fri Aug 23 15:08:28 2019 Received: from list by lists.gnu.org with archive (Exim 4.90_1) id 1i1EvE-0001DW-7l for mharc-axiom-developer@gnu.org; Fri, 23 Aug 2019 15:08:28 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:45617) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1i1EvA-00019L-Oo for axiom-developer@nongnu.org; Fri, 23 Aug 2019 15:08:25 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1i1Ev8-0003Rg-UK for axiom-developer@nongnu.org; Fri, 23 Aug 2019 15:08:24 -0400 Received: from mail-lf1-x133.google.com ([2a00:1450:4864:20::133]:39092) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1i1Ev8-0003Qy-Mk for axiom-developer@nongnu.org; Fri, 23 Aug 2019 15:08:22 -0400 Received: by mail-lf1-x133.google.com with SMTP id x3so7881646lfn.6 for ; Fri, 23 Aug 2019 12:08:22 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=KhhwXHqiHyfNQ5L2vGW1Egkqbz3qFCRrJtGZOTL44fg=; b=VNIrEkl5Sulgrg7YsfGb9XciqrBWj00MJ/iJFu33pW2kBE1Yie1zrkvJxjt2uxBodK A1zfROxhpDI4hY8zchSatQ2C5MDrFTy3S8dF4IEUjSLZyaX1kbKOmdj96KU7zzteGP6T KYpjHtO1vRnB7hJvyqcsIvUgTR0WSE1onUe16PgB7NOAerje8vu2v9qeTjIelyyL5a5d vWeEnRb+TmHmNgYLuOoaF7ZuEAX8rMjAcMtv7Af+Sl4YfpsrYUoQ6/wKzx2Twt7AZDWW ymmoKJstBbS8RUn/XuQ+/JFctArGO79o2hQxGZxpDhkaILZB3ICFBjpEs1ULI/YuuHHH HqKQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to; bh=KhhwXHqiHyfNQ5L2vGW1Egkqbz3qFCRrJtGZOTL44fg=; b=UC6xWoIbXnVLcVN8UX/OugQZqoNbJUEBv2Cu8d8JsPsVjorhig2CgB3HIUUhboqqPA LIJc95Z0EF8FU0Qzm3j2gQSaKrJBAiDKW8N5WBfI/2KrVwCOzHdD1j4vdlAunEqZRUNX PgmL2V83LzWyCH/TthdVEstTb41rAnyKJ/TbcmcAlj1ETi50PCUuKGuzOI8T3LQqRnFh 921yFJiTzFeEYa3l7TLa0bD7aaG62NeXS2MnuEH+a5HgLKwyspuhLdxdSYHp5s3yFPhi MzaIaBs0mreRjqJsPPrcVRWxBN2PQyqEEuU4nSTNMmo2YMKMMtn6/ySCLLdXZudMh88V DqBw== X-Gm-Message-State: APjAAAWv7xqHZLt5A4LRq4c/arORHklm/12ZkjuIlNxZ0EqJckCimcUp NqOqGB33dJGejCJii/SYdSm58DChe4BEZrTJ81GS5w== X-Google-Smtp-Source: APXvYqx+CjyCYTm3jKnQoGDrbuXm0ZP0AUmjhxURiaBI3wIPcUDLo/eKwQ8wxBf+Zc4jmmIHs/Hg3Epx/yW6DAopwQU= X-Received: by 2002:a05:6512:146:: with SMTP id m6mr3777088lfo.90.1566587299483; Fri, 23 Aug 2019 12:08:19 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:ab3:fcb:0:0:0:0:0 with HTTP; Fri, 23 Aug 2019 12:08:18 -0700 (PDT) In-Reply-To: References: From: Tim Daly Date: Fri, 23 Aug 2019 15:08:18 -0400 Message-ID: To: axiom-dev , Tim Daly Content-Type: text/plain; charset="UTF-8" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::133 Subject: Re: [Axiom-developer] Minor insight X-BeenThere: axiom-developer@nongnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Axiom Developers List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 23 Aug 2019 19:08:26 -0000 POS == Pile of Sand Since we only had 4K of memory, programmers used overlay linkers and include files. Include files were needed because compilers were single-pass and needed forward references. These "hacks" never died. Files were small, normally less than 4k for obvious reasons. If the file got too big the compiler choked, your flowchart generator failed, and you used too many punched cards. Sematics existed in 7 or 8 character file names and in variable name conventions (Fortran I-N were integers). Back in the day hard drives had gotten large enough that some bright-spot decided that a flat organization was bad. So they invented directories. These "hacks" never died. Of course, directories needed names but space was still tight so names were short but "meaningful", like src, doc, inc, etc. and a 'standard organization' was born. Your include files were looked for in 'inc', libraries in 'lib', etc. Once that standard was common, Stewart Feldman created 'make' to handle the complex task of finding and updating all of this nonsense. Now you could write down the way to build your program. (Now automake. Save us). Of course, the doc directory, then as now, is blank. So we have a history of sematics encoded in the whole directory.file.function.variable name, which should be good for any possible form of semantic transfer to any "real" programmer. Now we have "layered" IDEs on top of this POS pile and teach this to students as "the eternal way". But programs have outgrown this organization. Back in the day (said the old man), a "complex" program was 'grep' and an operating system could still be printed in a 30 page book. Whole compilers were printed in BYTE magazine. It isn't even the size of the listing that has outgrown the organization. It's the size of the ideas. I could read the PASCAL compiler source and have a clue. But I can't read the LEAN source. I can read C++, of course, but LEAN needs much more background 'theory' to begin to understand what rules the code implements. You don't write code just to get PROLOG to work. You write code to express an idea like 'functional prolog'. Anyone trying to read your source code without a lot of associated words would have no way to reverse engineer your Naur-like 'theory'. Yet you still use the POS orgainization rather than a literate program. You're writing to express an idea, a new theory, yet you bury most of it in 3 letter directories. Why? The machine doesn't care about your theory, the people do. Why are you writing for the machine? I should be able to sit and read your ideas with their associated source code in a single afternoon. Your source code is nothing more than the usual equations in a physics textbook. You could write a physics textbook without the equations but why? Creating a POS structure for the compiler from a literate program is trivial, a single command. Do you want me to REALLY understand linear logic? Write a distributed program with queues using linear logic and explain exactly what problem it solves and how it solves it. Show me ALL the code so I don't have to imagine it or dig it up out of the POS pile. Include the rules with their code implementation. Include chapters on theory and biblio references. Include a chapter of 'bad code' so I can compare it with your new theory. Communicate ideas to humans.Write literate code. I will try to turn your program into a literate form so you can see what I'm ranting about. Tim