# Axiom musings...

5 messages
Open this post in threaded view
|

## Axiom musings...

 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-37FE69F835BDD124It'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
Open this post in threaded view
|

## Re: Axiom musings...

 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-complexityUsing 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
Open this post in threaded view
|

## Re: Axiom musings...

 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