[Axiom-developer] Proving Axiom Correct

[Tim Daly]

I'm making progress on proving Axiom correct both at the Spad level and

the Lisp level. One interesting talk by Phillip Wadler on "Propositions as

Types", a very entertaining talk, is here:
https://www.youtube.com/watch?v=IOiZatlZtGU

He makes the interesting point late in the talk that some languages are

"discovered" based on fundamental logic principles (e.g.Lisp) and others

are "invented" with no formal basis (e.g. C). As he says, "you can tell

whether your language is discovered or invented".

The point is that Lisp has a formal logic basis and, as Spad is really

just a domain specific language implemented in Lisp then Spad shares

the formal logic basis.