Re: [open-axiom-devel] [Axiom-developer] Proving Axiom Correct
Gabriel Dos Reis <[email protected]>
| Newsgroups | gmane.comp.mathematics.open-axiom.devel,gmane.comp.mathematics.axiom.devel |
|---|---|
| Message-ID | <CAAiZkiBGhafviL9Mf_JRO+Cpns9yGHbWdmdp3K9-AC+1dCdsYA@mail.gmail.com> |
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 > > ------------------------------------------------------------------------------ Developer Access Program for Intel Xeon Phi Processors Access to Intel Xeon Phi processor-based developer platforms. With one year of Intel Parallel Studio XE. Training and support from Colfax. Order your platform today. http://sdm.link/xeonphi _______________________________________________ open-axiom-devel mailing list open-axiom-devel-5NWGOfrQmneRv+LV9MX5uipxlwaOVQ5f@public.gmane.org https://lists.sourceforge.net/lists/listinfo/open-axiom-devel