axiom-developer
[
Top
][
All Lists
]
Advanced
[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:
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.
reply via email to
[Prev in Thread]
Current Thread
[
Next in Thread
]
[Axiom-developer] Proving Axiom Correct
,
Tim Daly
<=
Re: [Axiom-developer] Proving Axiom Correct
,
Gabriel Dos Reis
,
2017/01/12
Re: [Axiom-developer] Proving Axiom Correct
,
Tim Daly
,
2017/01/13
Re: [Axiom-developer] Proving Axiom Correct
,
Kurt Pagani
,
2017/01/13
Re: [Axiom-developer] Proving Axiom Correct
,
Gabriel Dos Reis
,
2017/01/25
Re: [Axiom-developer] Proving Axiom Correct
,
Tim Daly
,
2017/01/25
Re: [Axiom-developer] Proving Axiom Correct
,
Tim Daly
,
2017/01/13
Next by Date:
Re: [Axiom-developer] Proving Axiom Correct
Next by thread:
Re: [Axiom-developer] Proving Axiom Correct
Index(es):
Date
Thread