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