[Top][All Lists]

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

Re: [Axiom-developer] Proving Axiom Correct

From: Gabriel Dos Reis
Subject: Re: [Axiom-developer] Proving Axiom Correct
Date: Thu, 12 Jan 2017 19:14:26 -0800

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 <address@hidden> 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:

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

reply via email to

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