There were implementations of C in Lisp. So C shares that formal logic basis, or that it was discovered?
On Wed, Jan 11, 2017 at 8:17 PM, Tim Daly <[email protected]> wrote: > 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 > [email protected] > https://lists.nongnu.org/mailman/listinfo/axiom-developer > >
_______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
