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 <axiom...@gmail.com> 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 Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer