Re: [EXTERNAL] Re: Axiom musings...

[Tim Daly]

Quoting Dijkstra (1988, EWD1036):

... a program is no more than half a conjecture. The other
half of a conjecture is the functional specification the
program is supposed to satisfy. The programmer's task
is to present such complete conjectures as proven theorems.


Axiom's SANE research project is trying to build a system
where such "complete conjectures as proven theorems"
can be implemented, at least for mathematical algorithms.

After 50 years of programming it is humbling to realize
that I've neglected the most important half of programming.

The amount of effort and progress in proof theory, category
theory, and interactive theorem proving is amazing; most
of it only occuring in this century. I've spent the last 8 years
trying to "catch up" with what future programmers will take
as normal and expected.

Imagine a Google whiteboard interview where you are
asked to provide an algorithm and an associated proof.
Will you get hired?

Dijkstra saw this in 1988 and it's taken me decades to
hear and understand.

Tim


On 12/18/20, Tim Daly <axiomcas@gmail.com> wrote:
> I occasionally get grief because Axiom is implemented
> in Common Lisp. People don't seem to like that for some
> odd reason. Lisp, one of the easiest languages to learn,
> seems to be difficult to accept.
>
> I'm working with John Harrison's book "Practical Logic
> and Automated Reasoning" from 2009. It uses OCaml
> to implement the programs.
>
> I've downloaded the OCaml sources from the website.
> Apparently OCaml has changed significantly from 2009
> since the code no longer compiles, spitting out "Alert
> deprecated" all over the place and simply failing in places.
>
> C++ code has a "standard", well, several "standards".
> When someone asks "Do you know C++" you really
> need to qualify that question. What you knew about
> "standard C++" seems to change every 2 years.
>
> I recently pulled out my KROPS code, used as the
> basis for IBM's Expert System FAME. It was written
> in Common Lisp (on a Symbolics machine). It still runs
> unmodified despite being written about 40 years ago
> on hardware and a software stack that no longer exists.
>
> Axiom, written in the last century, still compiles and
> runs. Say what you want about Lisp code, it still is the
> most portable and long-lasting language I've ever used.
>
> Tim
>