[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Proving Axiom Correct

From: Tim Daly
Subject: [Axiom-developer] Proving Axiom Correct
Date: Wed, 11 Jan 2017 23:17:20 -0500

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:

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.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]