Re: [Axiom-developer] Axiom musings...

[Tim Daly]

As you might expect, the new Axiom Sane effort is fully literate,
developed solely as a literate program.

One of the subgoals is to write a page per day. This can involve
explaining code. But it also involves explaining various ideas that
are related to the effort.

The current topic is a section on why this effort will fail. I have
been looking for various arguments from people who give
reasons why this effort cannot succeed.

For example, Ron Pressler seems to think that writing software
is beyond the difficulty of anything we've previously tried to do
and that math (alone) won't help us.
https://pron.github.io/posts/correctness-and-complexity

Using fundamental results from Godel and Turing, Ron seems
to show that software verification can't succeed. He may be
right in the general case.

Axiom isn't the general case. At least some of the algorithms
encode mathematics, a small subset of the universe of Ron's
argument and one where verification seems possible.

The Sane effort targets verification of the GCD algorithms in
Axiom. While this seems to be a trivial subset of Axiom with
a reasonably clear specification the effort is not trivial. The
overall goal involves restructuing Axiom so that the GCD
specification, verification, and proof occur "naturally" because
of design choices like inheriting axioms from Categories.

I strongly  recommend trying to verify programs. There is a
whole area of computational mathematics worth exploring.
The benefit is a much deeper understanding of your code.

In any case, it is certainly interesting to look for and write about
reasons why this is impossible.

It is also interesting to see the "intellectual space" opened up by
literate programming. Besides the usual "documentation", it provides
a space to discuss larger issues surrounding the problem to be solved.

I strongly recommend literate programming. Any program has a
lot of context, both with design ideas and supporting arguments.
Literate programs give "space" to present these to the reader.

And Axiom provides an "intellectual space" on the boundary between
mathematics and general purpose code. If verification can succeed,
Axiom is the ideal setting for experimentation.

There is no such thing as a simple job.
But this is certainly an interesting job.

Tim





On 8/4/19, Tim Daly <address@hidden> 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"
>